Language.Reflection.Pretty

Pretty Printing of Elab Data-Types

This module can be used in the repl to evaluate, how
syntax is translated to TTImp and Decl representations.
Use `putPretty` together with a quoted expression and
inspect the underlying implementation.

Note, to improve readability, some constructs are pretty printed
as infix operator chains. The operators in question can be found in
module `Language.Reflection.Syntax.Ops`.

REPL Examples:

  :exec putPretty `{{ Name.In.A.Namespace }}
  :exec putPretty `(Just (7 * x))
  :exec putPretty `((1 index : Fin n) -> Vect n t -> t)

Definitions

Opts80 : LayoutOpts

Totality: total
Visibility: public export

putDoc : HasIO io => Doc Opts80 -> io ()

  Pretty but uncolored output to the terminal

Totality: total
Visibility: export

putPretty : HasIO io => Pretty t => t -> io ()

  Pretty but uncolored output to the terminal

Totality: total
Visibility: export

0 WithName : Type -> Type

Totality: total
Visibility: public export

conH : All Pretty ts => Prec -> String -> All id ts -> Doc opts

Totality: total
Visibility: export

recordH : All Pretty ts => Prec -> String -> All WithName ts -> Doc opts

Totality: total
Visibility: export

op : Prec -> Nat -> Doc opts -> List (String, Doc opts) -> Doc opts

Totality: total
Visibility: export

prettyImplTTImp : Pretty TTImp

Totality: total
Visibility: export

prettyImplArg : Pretty Arg

Totality: total
Visibility: export

prettyImplClause : Pretty Clause

Totality: total
Visibility: export

prettyImplITy : Pretty ITy

Totality: total
Visibility: export