Derive.Neg

Definitions

minusClaim : Visibility -> Name -> ParamTypeInfo -> Decl

Totality: total
Visibility: export

negClaim : Visibility -> Name -> ParamTypeInfo -> Decl

Totality: total
Visibility: export

negImplClaim : Visibility -> Name -> ParamTypeInfo -> Decl

Totality: total
Visibility: export

minusDef : Name -> Con n vs -> Decl

Totality: total
Visibility: export

negDef : Name -> Con n vs -> Decl

Totality: total
Visibility: export

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

  Generate declarations and implementations for `Neg` for a
  single-constructor data type.

Totality: total
Visibility: export

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

  Alias for `NegVis Public`

Totality: total
Visibility: export