| 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