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

Safe HaskellSafe-Infered

Agda.TypeChecking.Pretty

Contents

Synopsis

Wrappers for pretty printing combinators

type Doc = DocSource

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

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

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

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

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

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

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

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

The PrettyTCM class