Derive.Pretty

Reexports

Definitions

data PlaceHolder : Type

Totality: total
Visibility: public export
Constructor: 

US : PlaceHolder

Hint: 

Pretty PlaceHolder

generalPrettyType : List Arg -> TTImp -> TTImp

  General type of a `prettyPrec` function with the given list
  of implicit and auto-implicit arguments, plus the given argument type
  to be displayed.

Totality: total
Visibility: export

prettyClaim : Visibility -> Name -> ParamTypeInfo -> Decl

  Top-level function declaration implementing the `prettyPrec` function for
  the given data type.

Totality: total
Visibility: export

prettyImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl

  Top-level declaration of the `Pretty` implementation for the given data type.

Totality: total
Visibility: export

prettyImplDef : Name -> Name -> Decl

  Top-level definition of the `Pretty` implementation for the given data type.

Totality: total
Visibility: export

prettyClauses : List Name -> Maybe Name -> TypeInfo -> List Clause

Totality: total
Visibility: export

prettyDef : List Name -> Name -> TypeInfo -> Decl

Totality: total
Visibility: export

derivePretty : Elab (Pretty f)

  Derive an implementation of `Pretty a` for a custom data type `a`.
  
  Note: This is mainly to be used for indexed data types. Consider using
        `derive` together with `Derive.Pretty.Pretty` for parameterized data types.

Totality: total
Visibility: export

PrettyVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)

  Generate declarations and implementations for `Pretty` for a given data type.

Totality: total
Visibility: export

Pretty : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Alias for `PrettyVis Public`

Totality: total
Visibility: export