prettyHiding info visible doc puts the correct braces
around doc according to info info and returns
visible doc if the we deal with a visible thing.
ModuleAgda-2.7.0.1Haskell2010
Agda.Syntax.Concrete.Pretty
Pretty printer for the concrete syntax.
- 2 types
- 17 values
- PackageAgda-2.7.0.1
- Exports19
- LanguageHaskell2010
- LicenceMIT
- SourcePretty.hs
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.
Constructors
Instances1Pretty
Pretty NamedBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pretty
module Agda.Syntax.Concrete.Glyph
Orphan instances
67 instancesShow BoundNameShow DeclarationShow DoStmtShow ExprShow LHSShow LHSCoreShow LamBindingShow LamClauseShow ModuleShow ModuleApplicationShow ModuleAssignmentShow PatternShow PragmaShow RHSShow TypedBindingShow WhereClausePretty AssociativityPretty CohesionPretty ErasedPretty FixityPretty Fixity'Pretty FixityLevelPretty LockPretty ModalityPretty NotationPartPretty Q0OriginPretty Q1OriginPretty QωOriginPretty QuantityPretty RelevancePretty 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 (Arg a)Pretty a => Pretty (MaybePlaceholder a)Pretty a => Pretty (WithHiding a)Pretty a => Pretty (Binder' a)Pretty a => Pretty (FieldAssignment' a)Pretty a => Pretty (TacticAttribute' a)Pretty e => Pretty (Named_ e)(Show a, Show b) => Show (ImportDirective' a b)(Show a, Show b) => Show (Renaming' a b)(Show a, Show b) => Show (Using' a b)(Pretty a, Pretty b) => Pretty (ImportDirective' a b)(Pretty a, Pretty b) => Pretty (ImportedName' a b)(Pretty a, Pretty b) => Pretty (Renaming' a b)(Pretty a, Pretty b) => Pretty (Using' a b)(Pretty a, Pretty b) => Pretty (Either a b)(Pretty a, Pretty b) => Pretty (a, b)