Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Pretty

Contents

Description

Pretty printer for the concrete syntax.

Synopsis

Documentation

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.

newtype Tel #

Constructors

Tel Telescope 

Instances

Pretty Tel # 

Methods

pretty :: Tel -> Doc #

prettyPrec :: Int -> Tel -> Doc #

Orphan instances

Show Pragma # 
Show ModuleApplication # 
Show Declaration # 
Show WhereClause # 
Show RHS # 

Methods

showsPrec :: Int -> RHS -> ShowS #

show :: RHS -> String #

showList :: [RHS] -> ShowS #

Show LHSCore # 
Show LHS # 

Methods

showsPrec :: Int -> LHS -> ShowS #

show :: LHS -> String #

showList :: [LHS] -> ShowS #

Show TypedBinding # 
Show TypedBindings # 
Show LamBinding # 
Show Pattern # 
Show Expr # 

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Pretty Fixity' # 

Methods

pretty :: Fixity' -> Doc #

prettyPrec :: Int -> Fixity' -> Doc #

Pretty Relevance # 
Pretty Induction # 
Pretty GenPart # 

Methods

pretty :: GenPart -> Doc #

prettyPrec :: Int -> GenPart -> Doc #

Pretty Notation # 

Methods

pretty :: Notation -> Doc #

prettyPrec :: Int -> Notation -> Doc #

Pretty Fixity # 

Methods

pretty :: Fixity -> Doc #

prettyPrec :: Int -> Fixity -> Doc #

Pretty Occurrence # 
Pretty Pragma # 

Methods

pretty :: Pragma -> Doc #

prettyPrec :: Int -> Pragma -> Doc #

Pretty OpenShortHand # 
Pretty ModuleApplication # 
Pretty Declaration # 
Pretty WhereClause # 
Pretty RHS # 

Methods

pretty :: RHS -> Doc #

prettyPrec :: Int -> RHS -> Doc #

Pretty LHSCore # 

Methods

pretty :: LHSCore -> Doc #

prettyPrec :: Int -> LHSCore -> Doc #

Pretty LHS # 

Methods

pretty :: LHS -> Doc #

prettyPrec :: Int -> LHS -> Doc #

Pretty TypedBinding # 
Pretty BoundName # 
Pretty TypedBindings # 
Pretty LamBinding # 
Pretty Pattern # 

Methods

pretty :: Pattern -> Doc #

prettyPrec :: Int -> Pattern -> Doc #

Pretty Expr # 

Methods

pretty :: Expr -> Doc #

prettyPrec :: Int -> Expr -> Doc #

Pretty ModuleAssignment # 
Pretty [Declaration] # 

Methods

pretty :: [Declaration] -> Doc #

prettyPrec :: Int -> [Declaration] -> Doc #

Pretty [Pattern] # 

Methods

pretty :: [Pattern] -> Doc #

prettyPrec :: Int -> [Pattern] -> Doc #

Pretty a => Pretty (MaybePlaceholder a) # 
Pretty e => Pretty (Named_ e) # 

Methods

pretty :: Named_ e -> Doc #

prettyPrec :: Int -> Named_ e -> Doc #

Pretty a => Pretty (Arg a) # 

Methods

pretty :: Arg a -> Doc #

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

Pretty a => Pretty (WithHiding a) # 

Methods

pretty :: WithHiding a -> Doc #

prettyPrec :: Int -> WithHiding a -> Doc #

Pretty (ThingWithFixity Name) # 
Pretty a => Pretty (FieldAssignment' a) # 
Pretty (OpApp Expr) # 

Methods

pretty :: OpApp Expr -> Doc #

prettyPrec :: Int -> OpApp Expr -> Doc #

(Pretty a, Pretty b) => Show (ImportDirective' a b) # 
(Pretty a, Pretty b) => Pretty (Either a b) # 

Methods

pretty :: Either a b -> Doc #

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

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

Methods

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

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

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

Methods

pretty :: ImportedName' a b -> Doc #

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

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

Methods

pretty :: Using' a b -> Doc #

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

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