Agda.TypeChecking.Pretty

Wrappers for pretty printing combinators

type Doc = Doc

empty :: TCM Doc

equals :: TCM Doc

colon :: TCM Doc

comma :: TCM Doc

pretty :: (Monad m, Pretty a) => a -> m Doc

prettyA :: (Pretty c, ToConcrete a c) => a -> TCM Doc

prettyAs :: (Pretty c, ToConcrete a [c]) => a -> TCM Doc

text :: String -> TCM Doc

pwords :: Monad m => String -> [m Doc]

fwords :: Monad m => String -> m Doc

sep :: [TCM Doc] -> TCM Doc

vcat :: [TCM Doc] -> TCM Doc

hsep :: [TCM Doc] -> TCM Doc

fsep :: [TCM Doc] -> TCM Doc

hcat :: (Monad f, Functor f) => [f Doc] -> f Doc

($$) :: TCM Doc -> TCM Doc -> TCM Doc

(<+>) :: TCM Doc -> TCM Doc -> TCM Doc

(<>) :: TCM Doc -> TCM Doc -> TCM Doc

($+$) :: TCM Doc -> TCM Doc -> TCM Doc

nest :: Functor f => Int -> f Doc -> f Doc

braces :: Functor f => f Doc -> f Doc

dbraces :: Functor f => f Doc -> f Doc

brackets :: Functor f => f Doc -> f Doc

parens :: Functor f => f Doc -> f Doc

prettyList :: [TCM Doc] -> TCMT IO Doc

punctuate :: TCM Doc -> [TCM Doc] -> [TCM Doc]

The PrettyTCM class

class PrettyTCM a where

Methods

prettyTCM :: a -> TCM Doc

Instances

PrettyTCM Bool

PrettyTCM Permutation

PrettyTCM Range

PrettyTCM Interval

PrettyTCM Position

PrettyTCM Nat

PrettyTCM Relevance

PrettyTCM Name

PrettyTCM ModuleName

PrettyTCM QName

PrettyTCM Name

PrettyTCM Literal

PrettyTCM Expr

PrettyTCM Pattern

PrettyTCM ClauseBody

PrettyTCM MetaId

PrettyTCM Level

PrettyTCM Sort

PrettyTCM Telescope

PrettyTCM Type

PrettyTCM Elim

PrettyTCM Term

PrettyTCM ConHead

PrettyTCM TCErr

PrettyTCM TypeError

PrettyTCM SplitError

PrettyTCM CallInfo

PrettyTCM Context

PrettyTCM Call

PrettyTCM Occurrence

PrettyTCM RewriteRule

PrettyTCM DisplayTerm

PrettyTCM TypeCheckingProblem

PrettyTCM Comparison

PrettyTCM Constraint

PrettyTCM ProblemConstraint

PrettyTCM NamedClause

PrettyTCM PrettyContext

PrettyTCM AsBinding

PrettyTCM DotPatternInst

PrettyTCM DeBruijnPat

PrettyTCM Node

PrettyTCM OccursWhere

PrettyTCM HypSizeConstraint

PrettyTCM SizeConstraint

Assumes we are in the right context.

PrettyTCM SizeMeta

PrettyTCM a => PrettyTCM [a]

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

PrettyTCM a => PrettyTCM (Blocked a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)

PrettyTCM a => PrettyTCM (MaybeReduced a)

PrettyTCM a => PrettyTCM (Closure a)

PrettyTCM a => PrettyTCM (HomHet a)

(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b)

(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e)

(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b)

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

PrettyTCM n => PrettyTCM (WithNode n Edge)

newtype PrettyContext

Constructors

PrettyContext Context

Instances

PrettyTCM PrettyContext