Text.Show.PrettyVal.Derive

Reexports

Definitions

rec : String -> List (Value, String) -> Value

  Displays an applied constructer in record syntax.
  This is called, if all arguments have user-defined names.
  Note: If the list of arguments is empty, this uses the
        `Con` data constructor in agreement with `parseValue`.

Visibility: public export

other : String -> List Value -> Value

Visibility: public export

generalPrettyValType : List Arg -> TTImp -> TTImp

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

Visibility: export

prettyValClaim : Name -> ParamTypeInfo -> Decl

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

Visibility: export

prettyValImplClaim : Name -> ParamTypeInfo -> Decl

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

Visibility: export

prettyValImplDef : Name -> Name -> Decl

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

Visibility: export

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

Visibility: export

prettyValDef : List Name -> Name -> TypeInfo -> Decl

Visibility: export

derivePrettyVal : Elab (PrettyVal f)

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

Visibility: export

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

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

Visibility: export