Agda.TypeChecking.Errors

Documentation

prettyError :: MonadTCM tcm => TCErr -> tcm String

class PrettyTCM a where

Methods

prettyTCM :: MonadTCM tcm => a -> tcm Doc

Instances

PrettyTCM Relevance

PrettyTCM ModuleName

PrettyTCM QName

PrettyTCM Name

PrettyTCM Literal

PrettyTCM MetaId

PrettyTCM ClauseBody

PrettyTCM Telescope

PrettyTCM Sort

PrettyTCM Type

PrettyTCM Term

PrettyTCM Expr

PrettyTCM TCErr

PrettyTCM TypeError

PrettyTCM Context

PrettyTCM Call

PrettyTCM DisplayTerm

PrettyTCM Comparison

PrettyTCM Constraint

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 b) => PrettyTCM (Judgement a b)

tcErrString :: TCErr -> String