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 = Doc

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

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

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

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

sep, vcat, hsep, fsep :: [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

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

The PrettyTCM class