diff options
Diffstat (limited to 'theories/Logic/DecidableTypeEx.v')
| -rw-r--r-- | theories/Logic/DecidableTypeEx.v | 24 |
1 files changed, 8 insertions, 16 deletions
diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v index 9c928598..9c59c519 100644 --- a/theories/Logic/DecidableTypeEx.v +++ b/theories/Logic/DecidableTypeEx.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableTypeEx.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: DecidableTypeEx.v 11699 2008-12-18 11:49:08Z letouzey $ *) Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. @@ -46,24 +46,16 @@ Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. Definition eq_dec := M.eq_dec. End Make_UDT. -(** An OrderedType can be seen as a DecidableType *) +(** An OrderedType can now directly be seen as a DecidableType *) -Module OT_as_DT (O:OrderedType) <: DecidableType. - Module OF := OrderedTypeFacts O. - Definition t := O.t. - Definition eq := O.eq. - Definition eq_refl := O.eq_refl. - Definition eq_sym := O.eq_sym. - Definition eq_trans := O.eq_trans. - Definition eq_dec := OF.eq_dec. -End OT_as_DT. +Module OT_as_DT (O:OrderedType) <: DecidableType := O. (** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) -Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT). -Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT). -Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT). -Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT). +Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. +Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. +Module N_as_DT <: UsualDecidableType := N_as_OT. +Module Z_as_DT <: UsualDecidableType := Z_as_OT. (** From two decidable types, we can build a new DecidableType over their cartesian product. *) @@ -99,7 +91,7 @@ End PairDecidableType. (** Similarly for pairs of UsualDecidableType *) -Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: DecidableType. +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := prod D1.t D2.t. Definition eq := @eq t. Definition eq_refl := @refl_equal t. |