Idris2Doc : Derive.ToJSON

Derive.ToJSON

(source)
Reexports
import public Derive.Show
Definitions
generalToJsonType : List Arg -> TTImp -> TTImp
  General type of a `toJSON` function with the given list
  of implicit and auto-implicit arguments, plus the given argument type
  to be displayed.
  
  TODO: Use fresh name for `v`

  Totality: total
  Visibility: export
toJsonClaim : Name -> ParamTypeInfo -> Decl
  Top-level function declaration implementing the `toJSON` function for
  the given data type.

  Totality: total
  Visibility: export
toJsonImplClaim : Name -> ParamTypeInfo -> Decl
  Top-level declaration of the `ToJSON` implementation for the given data type.

  Totality: total
  Visibility: export
toJsonImplDef : Name -> Name -> Decl
  Top-level definition of the `ToJSON` implementation for the given data type.

  Totality: total
  Visibility: export
toJsonClauses : List Name -> Options -> Name -> TypeInfo -> List Clause
  Totality: total
  Visibility: export
toJsonDef : List Name -> Options -> Name -> TypeInfo -> Decl
  Totality: total
  Visibility: export
customToJSON : Options -> List Name -> ParamTypeInfo -> Res (List TopLevel)
  Totality: total
  Visibility: export
ToJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
  Generate declarations and implementations for `ToJSON` for a given data type
  using default settings.

  Totality: total
  Visibility: export