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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Pretty

Contents

Synopsis

Wrappers for pretty printing combinators

type Doc = Doc Source

pretty :: Pretty a => a -> TCM Doc Source

prettyA :: (Pretty c, ToConcrete a c) => a -> TCM Doc Source

prettyAs :: (Pretty c, ToConcrete a [c]) => a -> TCM Doc Source

prettyList :: [TCM Doc] -> TCM Doc Source

Comma-separated list in brackets.

prettyList_ :: [TCM Doc] -> TCM Doc Source

prettyList without the brackets.

The PrettyTCM class

class PrettyTCM a where Source

Methods

prettyTCM :: a -> TCM Doc Source

Instances

PrettyTCM Bool Source 
PrettyTCM Range Source 
PrettyTCM MetaId Source 
PrettyTCM Nat Source 
PrettyTCM Relevance Source 
PrettyTCM QName Source 
PrettyTCM Name Source 
PrettyTCM ModuleName Source 
PrettyTCM QName Source 
PrettyTCM Name Source 
PrettyTCM Literal Source 
PrettyTCM Occurrence Source 
PrettyTCM Expr Source 
PrettyTCM Permutation Source 
PrettyTCM DeBruijnPattern Source 
PrettyTCM Pattern Source 
PrettyTCM ClauseBody Source 
PrettyTCM Clause Source 
PrettyTCM Level Source 
PrettyTCM Sort Source 
PrettyTCM Telescope Source 
PrettyTCM Type Source 
PrettyTCM Elim Source 
PrettyTCM Term Source 
PrettyTCM ConHead Source 
PrettyTCM Context Source 
PrettyTCM Polarity Source 
PrettyTCM RewriteRule Source 
PrettyTCM NLPat Source 
PrettyTCM DisplayTerm Source 
PrettyTCM TypeCheckingProblem Source 
PrettyTCM Comparison Source 
PrettyTCM Constraint Source 
PrettyTCM ProblemConstraint Source 
PrettyTCM ProblemId Source 
PrettyTCM NamedClause Source 
PrettyTCM PrettyContext Source 
PrettyTCM AsBinding Source 
PrettyTCM DotPatternInst Source 
PrettyTCM DeBruijnPat Source 
PrettyTCM Node Source 
PrettyTCM OccursWhere Source 
PrettyTCM HypSizeConstraint Source 
PrettyTCM SizeConstraint Source

Assumes we are in the right context.

PrettyTCM SizeMeta Source 
PrettyTCM SplitClause Source

For debugging only.

PrettyTCM a => PrettyTCM [a] Source 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source 
PrettyTCM a => PrettyTCM (WithHiding a) Source 
PrettyTCM a => PrettyTCM (Blocked a) Source 
PrettyTCM (Type' NLPat) Source 
PrettyTCM (Elim' NLPat) Source 
PrettyTCM (Elim' DisplayTerm) Source 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) Source 
PrettyTCM a => PrettyTCM (MaybeReduced a) Source 
PrettyTCM a => PrettyTCM (Judgement a) Source 
PrettyTCM a => PrettyTCM (Closure a) Source 
PrettyTCM a => PrettyTCM (Masked a) Source

Print masked things in double parentheses.

PrettyTCM a => PrettyTCM (HomHet a) Source 
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) Source 
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source 
PrettyTCM n => PrettyTCM (WithNode n Edge) Source 
(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c) Source 
(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n n e) Source 

showPat' :: (a -> TCM Doc) -> Pattern' a -> TCM Doc Source

Show a pattern, given a method how to show pattern variables.

data WithNode n a Source

Pairing something with a node (for printing only).

Constructors

WithNode n a