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

Timestamp:

Nov 11, 2010, 12:27:04 PM (10 years ago)

Author:

mulligan

Message:

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File:

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

Deliverables/D4.1/Matita/Nat.ma

@@ -50 +50 @@
 interpretation "Nat multiplication" 'times n m = (multiplication n m).
 
+nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝
+  match n with
+    [ Z ⇒ True
+    | S o ⇒
+      match m with
+        [ Z ⇒ False
+        | S p ⇒ less_than_or_equal o p
+        ]
+    ].
+    
+notation "n break ≤ m"
+  non associative with precedence 47
+  for @{ 'less_than_or_equal $n $m }.
+  
+interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m).
+
 nlemma plus_zero:
   ∀n: Nat.