Show the attributes necessary to recover a modality, in long-form (e.g. using at-syntax rather than dots). For the default modality, the result is at-ω (rather than the empty document). Suitable for showing modalities outside of binders.
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Concrete.Pretty
Pretty printer for the concrete syntax.
- 2 types
- 11 values
- PackageAgda-2.8.0.2
- Exports13
- LanguageHaskell2010
- LicenceMIT
- SourcePretty.hs
Constructors
Instances1Pretty
Pretty NamedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pretty
module Agda.Syntax.Concrete.Glyph
Orphan instances
44 instancesShow BoundNameShow DeclarationShow DoStmtShow ExprShow LHSShow LHSCoreShow LamBindingShow LamClauseShow ModuleShow ModuleApplicationShow ModuleAssignmentShow PatternShow PragmaShow RHSShow TypedBindingShow WhereClausePretty Fixity'Pretty NotationPartPretty BoundNamePretty DeclarationPretty DoStmtPretty ExprPretty LHSPretty LHSCorePretty LamBindingPretty LamClausePretty ModuleApplicationPretty ModuleAssignmentPretty OpenShortHandPretty PatternPretty PragmaPretty RHSPretty RecordDirectivePretty TypedBindingPretty WhereClauseShow a => Show (Binder' a)Show a => Show (OpApp a)Pretty (OpApp Expr)Pretty (ThingWithFixity Name)Pretty a => Pretty (MaybePlaceholder a)Pretty a => Pretty (Binder' a)Pretty a => Pretty (FieldAssignment' a)Pretty a => Pretty (TacticAttribute' a)(Pretty a, Pretty b) => Pretty (Either a b)