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

Safe Haskell | Safe-Infered

Agda.TypeChecking.Errors

# Documentation

prettyError :: TCErr -> TCM String

class PrettyTCM a where

Methods

prettyTCM :: a -> TCM Doc

Instances

PrettyTCM Relevance |
PrettyTCM ModuleName |
PrettyTCM QName |
PrettyTCM Name |
PrettyTCM Literal |
PrettyTCM MetaId |
PrettyTCM ClauseBody |
PrettyTCM Telescope |
PrettyTCM Level |
PrettyTCM Sort |
PrettyTCM Elim |
PrettyTCM Type |
PrettyTCM Term |
PrettyTCM Expr |
PrettyTCM TCErr |
PrettyTCM TypeError |
PrettyTCM Context |
PrettyTCM Call |
PrettyTCM DisplayTerm |
PrettyTCM Comparison |
PrettyTCM Constraint |
PrettyTCM ProblemConstraint |
PrettyTCM NamedClause |
PrettyTCM PrettyContext |
PrettyTCM Node |
PrettyTCM OccursWhere |
PrettyTCM DeBruijnPat |
PrettyTCM AsBinding |
PrettyTCM DotPatternInst |
PrettyTCM SplitError |
PrettyTCM a => PrettyTCM [a] |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) |
PrettyTCM a => PrettyTCM (Blocked a) |
PrettyTCM a => PrettyTCM (Closure a) |
PrettyTCM a => PrettyTCM (HomHet a) |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) |

tcErrString :: TCErr -> String