Idris2Doc : Derive.Finite

Derive.Finite

(source)
Reexports
import public Data.Finite
import public Derive.Prelude
Definitions
valuesClaim : Visibility -> Name -> ParamTypeInfo -> Decl
  Top-level function declaration implementing the `values` function for
  the given data type.

  Totality: total
  Visibility: export
finiteImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl
  Top-level declaration implementing the `Finite` interface for
  the given data type.

  Totality: total
  Visibility: export
finiteImplDef : Name -> Name -> Decl
  Totality: total
  Visibility: export
valuesDef : Name -> ParamTypeInfo -> Decl
  Definition of a (local or top-level) function implementing
  the values operation.

  Totality: total
  Visibility: export
FiniteVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
  Generate declarations and implementations for `Finite` for a given data type.

  Totality: total
  Visibility: export
Finite : List Name -> ParamTypeInfo -> Res (List TopLevel)
  Alias for `FiniteVis Public`

  Totality: total
  Visibility: export