PrettyTCM Bool Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Range Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Permutation Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM MetaId Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Nat Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Relevance Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM QName Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Name Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM ModuleName Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM QName Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Name Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Literal Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Term Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Occurrence Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM EqualityView Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM DBPatVar Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Clause Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Level Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Sort Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Telescope Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Type Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM ArgName Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Elim Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Term Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM ConHead Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM SplitTag Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM ProblemEq Source # | |
Instance detailsDefined in Agda.TypeChecking.Rules.LHS.Problem |
PrettyTCM TypedBinding Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Expr Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM TCErr Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM TypeError Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM UnificationFailure Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM NegativeUnification Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM SplitError Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM CallInfo Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM TCWarning Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM Warning Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM Call Source # | |
Instance detailsDefined in Agda.TypeChecking.Errors |
PrettyTCM IsForced Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Polarity Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM RewriteRule Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM NLPType Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM NLPat Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM DisplayTerm Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM TypeCheckingProblem Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Comparison Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM Constraint Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM ProblemConstraint Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM CheckpointId Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM ProblemId Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM NamedClause Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM PrettyContext Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM AbsurdPattern Source # | |
Instance detailsDefined in Agda.TypeChecking.Rules.LHS.Problem |
PrettyTCM DotPattern Source # | |
Instance detailsDefined in Agda.TypeChecking.Rules.LHS.Problem |
PrettyTCM AsBinding Source # | |
Instance detailsDefined in Agda.TypeChecking.Rules.LHS.Problem |
PrettyTCM ElimType Source # | |
Instance detailsDefined in Agda.TypeChecking.Records |
PrettyTCM Node Source # | |
Instance detailsDefined in Agda.TypeChecking.Positivity |
PrettyTCM SplitPatVar Source # | |
Instance detailsDefined in Agda.TypeChecking.Coverage.Match |
PrettyTCM ErrorPart Source # | |
Instance detailsDefined in Agda.TypeChecking.Unquote |
PrettyTCM HypSizeConstraint Source # | |
Instance detailsDefined in Agda.TypeChecking.SizedTypes.Solve |
PrettyTCM SizeConstraint Source # | Assumes we are in the right context. |
Instance detailsDefined in Agda.TypeChecking.SizedTypes.Solve |
PrettyTCM SizeMeta Source # | |
Instance detailsDefined in Agda.TypeChecking.SizedTypes.Solve |
PrettyTCM SplitClause Source # | For debugging only. |
Instance detailsDefined in Agda.TypeChecking.Coverage |
PrettyTCM a => PrettyTCM [a] Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM (Seq OccursWhere) Source # | |
Instance detailsDefined in Agda.TypeChecking.Positivity |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM a => PrettyTCM (WithHiding a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM (QNamed Clause) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM a => PrettyTCM (Pattern' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM a => PrettyTCM (Blocked a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM (Type' NLPat) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM (Elim' NLPat) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM (Elim' DisplayTerm) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM a => PrettyTCM (MaybeReduced a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM a => PrettyTCM (Judgement a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM a => PrettyTCM (Closure a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM a => PrettyTCM (Masked a) Source # | Print masked things in double parentheses. |
Instance detailsDefined in Agda.Termination.Monad |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source # | |
Instance detailsDefined in Agda.TypeChecking.Positivity |
(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |