| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Errors

Documentation

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

class PrettyTCM a where | Source

Methods

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

Instances

PrettyTCM Literal
PrettyTCM ModuleName
PrettyTCM QName
PrettyTCM Name
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 PrettyContext
PrettyTCM Node
PrettyTCM OccursWhere
PrettyTCM DeBruijnPat
PrettyTCM AsBinding
PrettyTCM DotPatternInst
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)

tcErrString :: TCErr -> String | Source

Produced by Haddock version 2.4.2