Derive.Ord

Definitions

ordClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

ordImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl

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

Totality: total
Visibility: export

ordImplDef : Name -> Name -> Decl

Totality: total
Visibility: export

ordClauses : List Name -> 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

ordDef : List Name -> Name -> Name -> TypeInfo -> Decl

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

  Alias for `OrdVis Public`

Totality: total
Visibility: export