Derive.HDecEq

Reexports

Definitions

hdeceqClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

hdeceqImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

hdeceqClauses : 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

hdeceqDef : Name -> TypeInfo -> Decl

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

Totality: total
Visibility: export

failEnum : Res a

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

  Alias for `EqVis Public`

Totality: total
Visibility: export