Derive.Show

Definitions

conWithArgs : Prec -> String -> List String -> String

Totality: total
Visibility: public export

recordWithArgs : Prec -> String -> List (String, String) -> String

Totality: total
Visibility: public export

namedArg : Arg -> Bool

  Checks, if the given argument is properly named.

Totality: total
Visibility: public export

generalShowType : List Arg -> TTImp -> TTImp

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

Totality: total
Visibility: export

showClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

showImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

showImplDef : Name -> Name -> Decl

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

showDef : List Name -> Name -> TypeInfo -> Decl

Totality: total
Visibility: export

deriveShow : Elab (Show f)

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

  Alias for `ShowVis Public`

Totality: total
Visibility: export