Derive.Eq

Definitions

conIndexName : Named a => a -> Name

Totality: total
Visibility: export

conIndexTypes : Nat -> (Bits32 -> TTImp, TTImp)

  Type used to represent the index of a data constructor.

Totality: total
Visibility: export

conIndexClauses : Named a => Name -> List a -> List Clause

  Clauses returning the index for each constructor in the given
  list.

Totality: total
Visibility: export

conIndexClaim : Visibility -> Name -> TypeInfo -> Decl

  Declaration of a function returning the constructor index
  for a value of the given data type.

Totality: total
Visibility: export

conIndexDef : Name -> TypeInfo -> Decl

  Definition of a function returning the constructor index
  for a value of the given data type.

Totality: total
Visibility: export

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

  For the given data type, creates a function for returning
  a 0-based index for each constructor.
  
  For instance, for `Either a b = Left a | Right b` this creates
  declarations as follows:
  
  ```idris
  conIndexEither : Either a b -> Bits8
  conIndexEither (Left {})  = 0
  conIndexEither (Right {}) = 1
  ```
  
  This function is useful in several situations: When deriving
  `Ord` for a sum type with more than one data constructors, we
  can use the constructor index to compare values created from
  distinct constructors. This allows us to only use a linear number
  of pattern matches to implement the ordering.
  
  For enum types (all data constructors have only erased arguments - if any),
  there are even greater benefits: `conIndex` is
  the identity function at runtime, being completely eliminated during
  code generations. This allows us to get `Eq` and `Ord` implementations for
  enum types, which run in O(1)!

Totality: total
Visibility: export

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

  Alias for `ConIndexVis Public`

Totality: total
Visibility: export

eqClaim : Visibility -> Name -> ParamTypeInfo -> Decl

  Top-level declaration implementing the equality test for
  the given data type.

Totality: total
Visibility: export

eqImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

eqClauses : List Name -> Name -> TypeInfo -> List Clause

  Generates pattern match clauses for the constructors of
  the given data type. `fun` is the name of the function we implement.
  This is either a local function definition in case of a
  custom derivation, or the name of a top-level function.

Totality: total
Visibility: export

eqDef : List Name -> Name -> TypeInfo -> Decl

  Definition of a (local or top-level) function implementing
  the equality check for the given data type.

Totality: total
Visibility: export

deriveEq : Elab (Eq f)

  Derive an implementation of `Eq a` for a custom data type `a`.
  
  Note: This is mainly to be used for indexed data types. Consider using
        `derive` together with `Derive.Eq.Eq` for parameterized data types.

Totality: total
Visibility: export

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

  Generate declarations and implementations for `Eq` for a given data type.

Totality: total
Visibility: export

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

  Alias for `EqVis Public`

Totality: total
Visibility: export