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

Safe HaskellNone

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 :: [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

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