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