aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-13 18:38:32 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-13 18:38:32 +0000
commit04b99a94d308eec12ecc7b0143122fe34d86ee90 (patch)
treefda1ec90d6f33803dbc505b7ef8540e85f14f5ec /theories
parentd357acaae5c2a27a4e3119879f02dbd39a0413c2 (diff)
Added the decidability of (<=) on nat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Classes/DecidableClass.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index 40543ac62..a03f15c42 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.v
@@ -81,6 +81,13 @@ split.
now destruct 1; symmetry; apply beq_nat_refl.
Qed.
+Program Instance Decidable_le_nat : forall (x y : nat), Decidable (x <= y) := {
+ Decidable_witness := leb x y
+}.
+Next Obligation.
+apply leb_iff.
+Qed.
+
Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
Decidable_witness := Zeq_bool x y
}.