diff options
Diffstat (limited to 'theories/NArith')
-rw-r--r-- | theories/NArith/NOrderedType.v | 16 | ||||
-rw-r--r-- | theories/NArith/POrderedType.v | 16 |
2 files changed, 14 insertions, 18 deletions
diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v index c47b4b4fe..08391d33f 100644 --- a/theories/NArith/NOrderedType.v +++ b/theories/NArith/NOrderedType.v @@ -13,19 +13,17 @@ Local Open Scope N_scope. (** * DecidableType structure for [N] binary natural numbers *) -Module N_as_MiniDT <: MiniDecidableType. +Module N_as_UBE <: UsualBoolEq. Definition t := N. - Definition eq_dec := N_eq_dec. -End N_as_MiniDT. - -Module N_as_DT <: UsualDecidableType. - Include Make_UDT N_as_MiniDT. + Definition eq := @eq N. Definition eqb := Neqb. Definition eqb_eq := Neqb_eq. -End N_as_DT. +End N_as_UBE. + +Module N_as_DT <: UsualDecidableTypeFull := Make_UDTF N_as_UBE. -(** Note that [N_as_DT] can also be seen as a [DecidableType] - and a [DecidableTypeOrig] and a [BooleanEqualityType] *) +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v index b5629eabe..85667e29a 100644 --- a/theories/NArith/POrderedType.v +++ b/theories/NArith/POrderedType.v @@ -13,20 +13,18 @@ Local Open Scope positive_scope. (** * DecidableType structure for [positive] numbers *) -Module Positive_as_MiniDT <: MiniDecidableType. +Module Positive_as_UBE <: UsualBoolEq. Definition t := positive. - Definition eq_dec := positive_eq_dec. -End Positive_as_MiniDT. - -Module Positive_as_DT <: UsualDecidableType. - Include Make_UDT Positive_as_MiniDT. + Definition eq := @eq positive. Definition eqb := Peqb. Definition eqb_eq := Peqb_eq. -End Positive_as_DT. +End Positive_as_UBE. +Module Positive_as_DT <: UsualDecidableTypeFull + := Make_UDTF Positive_as_UBE. -(** Note that [Positive_as_DT] can also be seen as a [DecidableType] - and a [DecidableTypeOrig] and a [BooleanEqualityType]. *) +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) |