PrettyTCM Bool Source # | |
|
PrettyTCM Range Source # | |
|
PrettyTCM Occurrence Source # | |
|
PrettyTCM Permutation 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 Term Source # | |
|
PrettyTCM Expr Source # | |
|
PrettyTCM EqualityView 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 CtxId 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 SplitClause Source # | For debugging only. |
|
PrettyTCM HypSizeConstraint Source # | |
|
PrettyTCM SizeConstraint Source # | Assumes we are in the right context. |
|
PrettyTCM SizeMeta Source # | |
|
PrettyTCM ErrorPart Source # | |
|
PrettyTCM a => PrettyTCM [a] Source # | |
|
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) 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 (WithHiding a) Source # | |
|
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # | |
|
PrettyTCM a => PrettyTCM (Blocked a) Source # | |
|
PrettyTCM (Type' NLPat) Source # | |
|
PrettyTCM (Elim' NLPat) Source # | |
|
PrettyTCM (Elim' DisplayTerm) 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 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 # | |
|