Idris2Doc : Derive.Enum

Derive.Enum

(source)
Reexports
import public Data.Enum
import public Derive.Finite
Definitions
conIndexLtName : Named a => a -> Name
  Totality: total
  Visibility: export
toIndexName : Named a => a -> Name
  Totality: total
  Visibility: export
toIndexInjectiveName : Named a => a -> Name
  Totality: total
  Visibility: export
valuesCompleteName : Named a => a -> Name
  Totality: total
  Visibility: export
conIndexLtClaim : Visibility -> Name -> Name -> TypeInfo -> Decl
  Top-level function declaration of a proof that all constructor indexes
  are less than the total number of constructors.

  Totality: total
  Visibility: export
toIndexInjectiveClaim : Visibility -> Name -> Name -> TypeInfo -> Decl
  Top-level function declaration of a proof that all the `conIndexXY`
  function is injective.

  Totality: total
  Visibility: export
valuesCompleteClaim : Visibility -> Name -> TypeInfo -> Decl
  Top-level function declaration of a proof that every value is
  indeed included in `Data.Finite.values`.

  Totality: total
  Visibility: export
toIndexClaim : Visibility -> Name -> TypeInfo -> Decl
  Top-level function declaration for a conversion of a data constructor
  to a value of type `Index n`, where `n` is the number of data constructors
  of the type.

  Totality: total
  Visibility: export
enumClaim : Visibility -> Name -> TypeInfo -> Decl
  Top-level `Enum` implementation declaration

  Totality: total
  Visibility: export
conIndexLtDef : Name -> TypeInfo -> Decl
  Totality: total
  Visibility: export
toIndexDef : Name -> Name -> Name -> Decl
  Totality: total
  Visibility: export
toIndexInjectiveDef : Name -> TypeInfo -> Decl
  Totality: total
  Visibility: export
valuesCompleteDef : Name -> TypeInfo -> Decl
  Totality: total
  Visibility: export
enumDef : Name -> Name -> Name -> Name -> Decl
  Totality: total
  Visibility: export
ConIndexLtVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
  Generates a proof that the constructor index returned by `conIndexXY` is
  strictly less than the number of constructors.

  Totality: total
  Visibility: export
ConIndexLt : List Name -> ParamTypeInfo -> Res (List TopLevel)
  Alias for `ConIndexLtVis Export`

  Totality: total
  Visibility: export
ToIndexVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
  Generates a conversion of data constructors to values of type `Index n`,
  where `n` is the number of data constructors of the given type.
  
  This includes `ConIndexLtVis`

  Totality: total
  Visibility: export
ToIndex : List Name -> ParamTypeInfo -> Res (List TopLevel)
  Alias for `ToIndexVis Export`

  Totality: total
  Visibility: export
ToIndexInjectiveVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
  Generates a proof that the `toIndexXY` function is injective.

  Totality: total
  Visibility: export
ToIndexInjective : List Name -> ParamTypeInfo -> Res (List TopLevel)
  Alias for `ToIndexInjectiveVis Export`

  Totality: total
  Visibility: export
ValuesCompleteVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
  Generates a proof that the `Data.Finite.values` indeed contains every
  possible value. This currently only works for enum types.

  Totality: total
  Visibility: export
ValuesComplete : List Name -> ParamTypeInfo -> Res (List TopLevel)
  Alias for `ValuesCompleteVis Export`

  Totality: total
  Visibility: export
EnumVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
  Derives interfaces `Eq`, `Ord`, `Finite`, and `Enum` plus utility
  functions with the relevant proofs for the given type.
  
  Erased proofs are generated at `export` visibility.

  Totality: total
  Visibility: export
Enum : List Name -> ParamTypeInfo -> Res (List TopLevel)
  Alias for `ValuesCompleteVis Export`

  Totality: total
  Visibility: export