Derive.FromJSON

Reexports

Definitions

generalFromJsonType : List Arg -> TTImp -> TTImp

  General type of a `fromJSON` function with the given list
  of implicit and auto-implicit arguments, plus the given argument type
  to be displayed.
  
  TODO: Use fresh names for `v` and `obj`.

Totality: total
Visibility: export

fromJsonClaim : Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

fromJsonImplClaim : Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

fromJsonImplDef : Name -> Name -> Decl

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

Totality: total
Visibility: export

fromJsonClause : List Name -> Options -> TTImp -> TTImp -> Name -> TypeInfo -> Clause

Totality: total
Visibility: export

fromJsonDef : List Name -> Options -> TTImp -> TTImp -> Name -> TypeInfo -> Decl

Totality: total
Visibility: export

customFromJSON : Options -> List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export

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

  Generate declarations and implementations for
  `FromJSON` for a given data type
  using default settings.

Totality: total
Visibility: export