Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Pretty

Contents

- Wrappers for pretty printing combinators
- The PrettyTCM class

Synopsis

- 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
- 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
- ($$) :: 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]
- class PrettyTCM a where
  - prettyTCM :: a -> TCM Doc
- newtype PrettyContext = PrettyContext Context

# 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

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

($$) :: 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 Nat |
PrettyTCM Relevance |
PrettyTCM Name |
PrettyTCM ModuleName |
PrettyTCM QName |
PrettyTCM Name |
PrettyTCM Literal |
PrettyTCM ClauseBody |
PrettyTCM MetaId |
PrettyTCM Level |
PrettyTCM Sort |
PrettyTCM Telescope |
PrettyTCM Type |
PrettyTCM Elim |
PrettyTCM Term |
PrettyTCM Expr |
PrettyTCM TCErr |
PrettyTCM TypeError |
PrettyTCM Context |
PrettyTCM Call |
PrettyTCM Occurrence |
PrettyTCM DisplayTerm |
PrettyTCM Comparison |
PrettyTCM Constraint |
PrettyTCM ProblemConstraint |
PrettyTCM NamedClause |
PrettyTCM PrettyContext |
PrettyTCM Node |
PrettyTCM OccursWhere |
PrettyTCM AsBinding |
PrettyTCM DotPatternInst |
PrettyTCM SplitError |
PrettyTCM DeBruijnPat |
PrettyTCM a => PrettyTCM [a] |
(ReifyWhen a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) |
PrettyTCM a => PrettyTCM (Blocked a) |
PrettyTCM a => PrettyTCM (Closure a) |
PrettyTCM a => PrettyTCM (HomHet a) |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) |
PrettyTCM n => PrettyTCM (n, Occurrence) |
PrettyTCM n => PrettyTCM (n, Edge) |
(PrettyTCM n, PrettyTCM (n, e)) => PrettyTCM (Graph n e) |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named String a) |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) |

newtype PrettyContext

Constructors

PrettyContext Context |

Instances

PrettyTCM PrettyContext |