Agda.Utils.Pretty

Pretty printing functions.

Documentation

class Pretty a where

Methods

pretty :: a -> Doc

prettyPrec :: Int -> a -> Doc

Instances

Pretty String

Pretty Doc

Pretty Relevance

Pretty Induction

Pretty TopLevelModuleName

Pretty QName

Pretty Name

Pretty Fixity

Pretty Order

Pretty CallMatrix

Pretty Literal

Pretty Pragma

Pretty OpenShortHand

Pretty ModuleApplication

Pretty Declaration

Pretty ImportedName

Pretty UsingOrHiding

Pretty ImportDirective

Pretty WhereClause

Pretty RHS

Pretty LHSCore

Pretty LHS

Pretty ColoredTypedBinding

Pretty TypedBinding

Pretty BoundName

Pretty TypedBindings

Pretty LamBinding

Pretty Pattern

Pretty Expr

Pretty Tel

Pretty LevelAtom

Pretty PlusLevel

Pretty Level

Pretty Sort

Pretty Type

Pretty Elim

Pretty Term

Pretty CompiledClauses

Pretty CallInfo

Pretty CallPath

Only show intermediate nodes. (Drop last CallInfo).

Pretty [Declaration]

Pretty [Pattern]

Pretty a => Pretty (Lisp a)

Pretty e => Pretty (Named_ e)

Pretty (ThingWithFixity Name)

Pretty cinfo => Pretty (CMSet cinfo)

Pretty cinfo => Pretty (CallMatrixAug cinfo)

Pretty cinfo => Pretty (CallGraph cinfo)

Displays the recursion behaviour corresponding to a call graph.

Pretty (OpApp Expr)

Pretty e => Pretty (Arg e)

Pretty a => Pretty (Arg a)

Pretty a => Pretty (Case a)

Pretty a => Pretty (WithArity a)

(Pretty a, Pretty b) => Pretty (a, b)

(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b)

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b)

pwords :: String -> [Doc]

fwords :: String -> Doc

mparens :: Bool -> Doc -> Doc

align :: Int -> [(String, Doc)] -> Doc

align max rows lays out the elements of rows in two columns, with the second components aligned. The alignment column of the second components is at most max characters to the right of the left-most column.

Precondition: max > 0.