Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Pretty

Description

Pretty printer for the concrete syntax.

Synopsis

Documentation

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

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.

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

attributesForModality :: Modality -> Doc Source #

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.

newtype Tel Source #

Constructors

Tel Telescope 

Instances

Instances details
Pretty Tel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Orphan instances

Pretty Associativity Source # 
Instance details

Pretty Cohesion Source # 
Instance details

Pretty Erased Source # 
Instance details

Pretty Fixity Source # 
Instance details

Pretty Fixity' Source # 
Instance details

Pretty FixityLevel Source # 
Instance details

Pretty Modality Source # 
Instance details

Pretty NotationPart Source # 
Instance details

Pretty Q0Origin Source # 
Instance details

Pretty Q1Origin Source # 
Instance details

Pretty Quantity Source # 
Instance details

Pretty QωOrigin Source # 
Instance details

Pretty Relevance Source # 
Instance details

Pretty BoundName Source # 
Instance details

Pretty Declaration Source # 
Instance details

Pretty DoStmt Source # 
Instance details

Pretty Expr Source # 
Instance details

Pretty LHS Source # 
Instance details

Pretty LHSCore Source # 
Instance details

Pretty LamBinding Source # 
Instance details

Pretty LamClause Source # 
Instance details

Pretty ModuleApplication Source # 
Instance details

Pretty ModuleAssignment Source # 
Instance details

Pretty OpenShortHand Source # 
Instance details

Pretty Pattern Source # 
Instance details

Pretty Pragma Source # 
Instance details

Pretty RHS Source # 
Instance details

Pretty TypedBinding Source # 
Instance details

Pretty WhereClause Source # 
Instance details

Show BoundName Source # 
Instance details

Show Declaration Source # 
Instance details

Show DoStmt Source # 
Instance details

Show Expr Source # 
Instance details

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Show LHS Source # 
Instance details

Methods

showsPrec :: Int -> LHS -> ShowS #

show :: LHS -> String #

showList :: [LHS] -> ShowS #

Show LHSCore Source # 
Instance details

Show LamBinding Source # 
Instance details

Show LamClause Source # 
Instance details

Show Module Source # 
Instance details

Show ModuleApplication Source # 
Instance details

Show ModuleAssignment Source # 
Instance details

Show Pattern Source # 
Instance details

Show Pragma Source # 
Instance details

Show RHS Source # 
Instance details

Methods

showsPrec :: Int -> RHS -> ShowS #

show :: RHS -> String #

showList :: [RHS] -> ShowS #

Show TypedBinding Source # 
Instance details

Show WhereClause Source # 
Instance details

Pretty a => Pretty (Arg a) Source # 
Instance details

Methods

pretty :: Arg a -> Doc Source #

prettyPrec :: Int -> Arg a -> Doc Source #

prettyList :: [Arg a] -> Doc Source #

Pretty a => Pretty (MaybePlaceholder a) Source # 
Instance details

Pretty e => Pretty (Named_ e) Source # 
Instance details

Pretty a => Pretty (WithHiding a) Source # 
Instance details

Pretty a => Pretty (Binder' a) Source # 
Instance details

Pretty a => Pretty (FieldAssignment' a) Source # 
Instance details

Pretty (OpApp Expr) Source # 
Instance details

Pretty (ThingWithFixity Name) Source # 
Instance details

Show a => Show (Binder' a) Source # 
Instance details

Methods

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

show :: Binder' a -> String #

showList :: [Binder' a] -> ShowS #

Show a => Show (OpApp a) Source # 
Instance details

Methods

showsPrec :: Int -> OpApp a -> ShowS #

show :: OpApp a -> String #

showList :: [OpApp a] -> ShowS #

(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # 
Instance details

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # 
Instance details

(Pretty a, Pretty b) => Pretty (Using' a b) Source # 
Instance details

Methods

pretty :: Using' a b -> Doc Source #

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

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

(Pretty a, Pretty b) => Pretty (Either a b) Source # 
Instance details

Methods

pretty :: Either a b -> Doc Source #

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

prettyList :: [Either a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (a, b) Source # 
Instance details

Methods

pretty :: (a, b) -> Doc Source #

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

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

(Show a, Show b) => Show (ImportDirective' a b) Source # 
Instance details

(Show a, Show b) => Show (Renaming' a b) Source # 
Instance details

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) Source # 
Instance details

Methods

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

show :: Using' a b -> String #

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