Derive.Num

Definitions

pmClaim : Visibility -> Name -> ParamTypeInfo -> Decl

  Top-level declaration implementing used for `(+)` and `(*)` functions for
  the given data type.

Totality: total
Visibility: export

fromIntClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

numImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl

  Top-level declaration implementing the `Eq` interface for
  the given data type.

Totality: total
Visibility: export

plusDef : Name -> Con n vs -> Decl

Totality: total
Visibility: export

multDef : Name -> Con n vs -> Decl

Totality: total
Visibility: export

fromIntDef : Name -> Con n vs -> Decl

Totality: total
Visibility: export

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

  Generate declarations and implementations for `Num` for a
  single-constructor data type.

Totality: total
Visibility: export

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

  Alias for `NumVis Public`

Totality: total
Visibility: export

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

  Generate a single `fromInteger` function for the given type

Totality: total
Visibility: export

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

  Generate a single `fromInteger` function with `public export`
  visibility for the given type

Totality: total
Visibility: export