Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Pretty
Contents
Wrappers for pretty printing combinators
The PrettyTCM class
Synopsis
type
Doc
=
Doc
comma
::
MonadTCM
tcm => tcm
Doc
empty
::
MonadTCM
tcm => tcm
Doc
class
PrettyTCM
a
where
prettyTCM
::
MonadTCM
tcm => a -> tcm
Doc
newtype
PrettyContext
=
PrettyContext
Context
Wrappers for pretty printing combinators
type
Doc
=
Doc
Source
comma
::
MonadTCM
tcm => tcm
Doc
Source
empty
::
MonadTCM
tcm => tcm
Doc
Source
The PrettyTCM class
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)
newtype
PrettyContext
Source
Constructors
PrettyContext
Context
Instances
PrettyTCM
PrettyContext
Produced by
Haddock
version 2.4.2