Changeset 275 for Deliverables/D4.1/Matita/Nat.ma

Timestamp:

Nov 24, 2010, 3:40:37 PM (10 years ago)

Author:

mulligan

Message:

Removed all axioms from Arithmetic.ma and replaced them with implemented functions from other files. Implemented decidable equality on Nats.

File:

• Deliverables/D4.1/Matita/Nat.ma (modified) (2 diffs)

Deliverables/D4.1/Matita/Nat.ma

@@ -43 +43 @@
     n ≤ m.
 
-ndefinition greater_than_or_equal_b ≝
+ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
   λm, n: Nat.
     n ≤ m.
@@ -190 +190 @@
 interpretation "Nat exponential" 'exponential n m = (exponential n m).
 
+nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝
+  match m with
+    [ Z ⇒
+      match n with
+        [ Z ⇒ true
+        | _ ⇒ false
+        ]
+    | S o ⇒
+      match n with
+        [ S p ⇒ decidable_equality o p
+        | _ ⇒ false
+        ]
+    ].
+
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 (* Greatest common divisor and least common multiple.                         *)