Agda.Syntax.Concrete.Pretty

Pretty printer for the concrete syntax.

Documentation

newtype Tel

Constructors

Tel Telescope

Instances

Pretty Tel

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Tel -> Doc

prettyPrec :: Int -> Tel -> Doc

prettyList :: [Tel] -> Doc

data NamedBinding

Constructors

NamedBinding

Fields

• withHiding :: Bool
• namedBinding :: NamedArg Binder

Instances

Pretty NamedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: NamedBinding -> Doc

prettyPrec :: Int -> NamedBinding -> Doc

prettyList :: [NamedBinding] -> Doc

prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc

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.

prettyRelevance :: LensRelevance a => a -> Doc -> Doc

bracesAndSemicolons :: Foldable t => t Doc -> Doc

prettyQuantity :: LensQuantity a => a -> Doc -> Doc

prettyLock :: LensLock a => a -> Doc -> Doc

prettyErased :: Erased -> Doc -> Doc

prettyCohesion :: LensCohesion a => a -> Doc -> Doc

prettyTactic :: BoundName -> Doc -> Doc

prettyTactic' :: TacticAttribute -> Doc -> Doc

prettyFiniteness :: BoundName -> Doc -> Doc

attributesForModality :: Modality -> Doc

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.

prettyOpApp :: forall a. Pretty a => Aspect -> QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]

smashTel :: Telescope -> Telescope

isLabeled :: NamedArg Binder -> Maybe ArgName

pRecord :: Erased -> Name -> RecordDirectives -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc

pRecordDirective :: RecordDirective -> Doc

pHasEta0 :: HasEta0 -> Doc

module Agda.Syntax.Concrete.Glyph

Orphan instances

Pretty Associativity

Methods

pretty :: Associativity -> Doc

prettyPrec :: Int -> Associativity -> Doc

prettyList :: [Associativity] -> Doc

Pretty Cohesion

Methods

pretty :: Cohesion -> Doc

prettyPrec :: Int -> Cohesion -> Doc

prettyList :: [Cohesion] -> Doc

Pretty Erased

Methods

pretty :: Erased -> Doc

prettyPrec :: Int -> Erased -> Doc

prettyList :: [Erased] -> Doc

Pretty Fixity

Methods

pretty :: Fixity -> Doc

prettyPrec :: Int -> Fixity -> Doc

prettyList :: [Fixity] -> Doc

Pretty Fixity'

Methods

pretty :: Fixity' -> Doc

prettyPrec :: Int -> Fixity' -> Doc

prettyList :: [Fixity'] -> Doc

Pretty FixityLevel

Methods

pretty :: FixityLevel -> Doc

prettyPrec :: Int -> FixityLevel -> Doc

prettyList :: [FixityLevel] -> Doc

Pretty Modality

Methods

pretty :: Modality -> Doc

prettyPrec :: Int -> Modality -> Doc

prettyList :: [Modality] -> Doc

Pretty NotationPart

Methods

pretty :: NotationPart -> Doc

prettyPrec :: Int -> NotationPart -> Doc

prettyList :: [NotationPart] -> Doc

Pretty Q0Origin

Methods

pretty :: Q0Origin -> Doc

prettyPrec :: Int -> Q0Origin -> Doc

prettyList :: [Q0Origin] -> Doc

Pretty Q1Origin

Methods

pretty :: Q1Origin -> Doc

prettyPrec :: Int -> Q1Origin -> Doc

prettyList :: [Q1Origin] -> Doc

Pretty Quantity

Methods

pretty :: Quantity -> Doc

prettyPrec :: Int -> Quantity -> Doc

prettyList :: [Quantity] -> Doc

Pretty QωOrigin

Methods

pretty :: QωOrigin -> Doc

prettyPrec :: Int -> QωOrigin -> Doc

prettyList :: [QωOrigin] -> Doc

Pretty Relevance

Methods

pretty :: Relevance -> Doc

prettyPrec :: Int -> Relevance -> Doc

prettyList :: [Relevance] -> Doc

Pretty BoundName

Methods

pretty :: BoundName -> Doc

prettyPrec :: Int -> BoundName -> Doc

prettyList :: [BoundName] -> Doc

Pretty Declaration

Methods

pretty :: Declaration -> Doc

prettyPrec :: Int -> Declaration -> Doc

prettyList :: [Declaration] -> Doc

Pretty DoStmt

Methods

pretty :: DoStmt -> Doc

prettyPrec :: Int -> DoStmt -> Doc

prettyList :: [DoStmt] -> Doc

Pretty Expr

Methods

pretty :: Expr -> Doc

prettyPrec :: Int -> Expr -> Doc

prettyList :: [Expr] -> Doc

Pretty LHS

Methods

pretty :: LHS -> Doc

prettyPrec :: Int -> LHS -> Doc

prettyList :: [LHS] -> Doc

Pretty LHSCore

Methods

pretty :: LHSCore -> Doc

prettyPrec :: Int -> LHSCore -> Doc

prettyList :: [LHSCore] -> Doc

Pretty LamBinding

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

Pretty LamClause

Methods

pretty :: LamClause -> Doc

prettyPrec :: Int -> LamClause -> Doc

prettyList :: [LamClause] -> Doc

Pretty ModuleApplication

Methods

pretty :: ModuleApplication -> Doc

prettyPrec :: Int -> ModuleApplication -> Doc

prettyList :: [ModuleApplication] -> Doc

Pretty ModuleAssignment

Methods

pretty :: ModuleAssignment -> Doc

prettyPrec :: Int -> ModuleAssignment -> Doc

prettyList :: [ModuleAssignment] -> Doc

Pretty OpenShortHand

Methods

pretty :: OpenShortHand -> Doc

prettyPrec :: Int -> OpenShortHand -> Doc

prettyList :: [OpenShortHand] -> Doc

Pretty Pattern

Methods

pretty :: Pattern -> Doc

prettyPrec :: Int -> Pattern -> Doc

prettyList :: [Pattern] -> Doc

Pretty Pragma

Methods

pretty :: Pragma -> Doc

prettyPrec :: Int -> Pragma -> Doc

prettyList :: [Pragma] -> Doc

Pretty RHS

Methods

pretty :: RHS -> Doc

prettyPrec :: Int -> RHS -> Doc

prettyList :: [RHS] -> Doc

Pretty TypedBinding

Methods

pretty :: TypedBinding -> Doc

prettyPrec :: Int -> TypedBinding -> Doc

prettyList :: [TypedBinding] -> Doc

Pretty WhereClause

Methods

pretty :: WhereClause -> Doc

prettyPrec :: Int -> WhereClause -> Doc

prettyList :: [WhereClause] -> Doc

Show BoundName

Methods

showsPrec :: Int -> BoundName -> ShowS

show :: BoundName -> String

showList :: [BoundName] -> ShowS

Show Declaration

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Show DoStmt

Methods

showsPrec :: Int -> DoStmt -> ShowS

show :: DoStmt -> String

showList :: [DoStmt] -> ShowS

Show Expr

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Show LHS

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

Show LHSCore

Methods

showsPrec :: Int -> LHSCore -> ShowS

show :: LHSCore -> String

showList :: [LHSCore] -> ShowS

Show LamBinding

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Show LamClause

Methods

showsPrec :: Int -> LamClause -> ShowS

show :: LamClause -> String

showList :: [LamClause] -> ShowS

Show Module

Methods

showsPrec :: Int -> Module -> ShowS

show :: Module -> String

showList :: [Module] -> ShowS

Show ModuleApplication

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

Show ModuleAssignment

Methods

showsPrec :: Int -> ModuleAssignment -> ShowS

show :: ModuleAssignment -> String

showList :: [ModuleAssignment] -> ShowS

Show Pattern

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

Show Pragma

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

Show RHS

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

Show TypedBinding

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

Show WhereClause

Methods

showsPrec :: Int -> WhereClause -> ShowS

show :: WhereClause -> String

showList :: [WhereClause] -> ShowS

Pretty a => Pretty (Arg a)

Methods

pretty :: Arg a -> Doc

prettyPrec :: Int -> Arg a -> Doc

prettyList :: [Arg a] -> Doc

Pretty a => Pretty (MaybePlaceholder a)

Methods

pretty :: MaybePlaceholder a -> Doc

prettyPrec :: Int -> MaybePlaceholder a -> Doc

prettyList :: [MaybePlaceholder a] -> Doc

Pretty e => Pretty (Named_ e)

Methods

pretty :: Named_ e -> Doc

prettyPrec :: Int -> Named_ e -> Doc

prettyList :: [Named_ e] -> Doc

Pretty a => Pretty (WithHiding a)

Methods

pretty :: WithHiding a -> Doc

prettyPrec :: Int -> WithHiding a -> Doc

prettyList :: [WithHiding a] -> Doc

Pretty a => Pretty (Binder' a)

Methods

pretty :: Binder' a -> Doc

prettyPrec :: Int -> Binder' a -> Doc

prettyList :: [Binder' a] -> Doc

Pretty a => Pretty (FieldAssignment' a)

Methods

pretty :: FieldAssignment' a -> Doc

prettyPrec :: Int -> FieldAssignment' a -> Doc

prettyList :: [FieldAssignment' a] -> Doc

Pretty (OpApp Expr)

Methods

pretty :: OpApp Expr -> Doc

prettyPrec :: Int -> OpApp Expr -> Doc

prettyList :: [OpApp Expr] -> Doc

Pretty (ThingWithFixity Name)

Methods

pretty :: ThingWithFixity Name -> Doc

prettyPrec :: Int -> ThingWithFixity Name -> Doc

prettyList :: [ThingWithFixity Name] -> Doc

Show a => Show (Binder' a)

Methods

showsPrec :: Int -> Binder' a -> ShowS

show :: Binder' a -> String

showList :: [Binder' a] -> ShowS

Show a => Show (OpApp a)

Methods

showsPrec :: Int -> OpApp a -> ShowS

show :: OpApp a -> String

showList :: [OpApp a] -> ShowS

(Pretty a, Pretty b) => Pretty (ImportDirective' a b)

Methods

pretty :: ImportDirective' a b -> Doc

prettyPrec :: Int -> ImportDirective' a b -> Doc

prettyList :: [ImportDirective' a b] -> Doc

(Pretty a, Pretty b) => Pretty (ImportedName' a b)

Methods

pretty :: ImportedName' a b -> Doc

prettyPrec :: Int -> ImportedName' a b -> Doc

prettyList :: [ImportedName' a b] -> Doc

(Pretty a, Pretty b) => Pretty (Renaming' a b)

Methods

pretty :: Renaming' a b -> Doc

prettyPrec :: Int -> Renaming' a b -> Doc

prettyList :: [Renaming' a b] -> Doc

(Pretty a, Pretty b) => Pretty (Using' a b)

Methods

pretty :: Using' a b -> Doc

prettyPrec :: Int -> Using' a b -> Doc

prettyList :: [Using' a b] -> Doc

(Pretty a, Pretty b) => Pretty (Either a b)

Methods

pretty :: Either a b -> Doc

prettyPrec :: Int -> Either a b -> Doc

prettyList :: [Either a b] -> Doc

(Pretty a, Pretty b) => Pretty (a, b)

Methods

pretty :: (a, b) -> Doc

prettyPrec :: Int -> (a, b) -> Doc

prettyList :: [(a, b)] -> Doc

(Show a, Show b) => Show (ImportDirective' a b)

Methods

showsPrec :: Int -> ImportDirective' a b -> ShowS

show :: ImportDirective' a b -> String

showList :: [ImportDirective' a b] -> ShowS

(Show a, Show b) => Show (Renaming' a b)

Methods

showsPrec :: Int -> Renaming' a b -> ShowS

show :: Renaming' a b -> String

showList :: [Renaming' a b] -> ShowS

(Show a, Show b) => Show (Using' a b)

Methods

showsPrec :: Int -> Using' a b -> ShowS

show :: Using' a b -> String

showList :: [Using' a b] -> ShowS