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

Timestamp:

Nov 12, 2010, 4:51:45 PM (11 years ago)

Author:

mulligan

Message:

More functions on bitvectors written.

File:

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

Deliverables/D4.1/Matita/Nat.ma

@@ -34 +34 @@
     ].
     
-notation "n break ≤ m"
+notation "hvbox(n break ≤ m)"
   non associative with precedence 47
   for @{ 'less_than_or_equal $n $m }.
@@ -49 +49 @@
     n ≤ m.
     
-notation "n break ≥ m"
+notation "hvbox(n break ≥ m)"
   non associative with precedence 47
   for @{ 'greater_than_or_equal $n $m }.
@@ -62 +62 @@
     m ≤ n ∧ ¬(m = n).
     
-notation "n break < m"
+notation "hvbox(n break < m)"
   non associative with precedence 47
   for @{ 'less_than $n $m }.
@@ -72 +72 @@
     n < m.
     
-notation "n break > m"
+notation "hvbox(n break > m)"
   non associative with precedence 47
   for @{ 'greater_than $n $m }.
@@ -87 +87 @@
     ].
     
-notation "n break + m"
+notation "hvbox(n break + m)"
   right associative with precedence 52
   for @{ 'plus $n $m }.
@@ -103 +103 @@
     ].
     
-notation "n break - m"
+notation "hvbox(n break - m)"
   right associative with precedence 47
   for @{ 'minus $n $m }.
@@ -119 +119 @@
     ].
     
-notation "n break * m"
+notation "hvbox(n break * m)"
   right associative with precedence 47
   for @{ 'multiplication $n $m }.
@@ -142 +142 @@
       ].
       
-notation "n break ÷ m"
+notation "hvbox(n break ÷ m)"
   right associative with precedence 47
   for @{ 'division $n $m }.
@@ -165 +165 @@
       ].
     
-notation "n break % m"
+notation "hvbox(n break % m)"
   right associative with precedence 47
   for @{ 'modulus $n $m }.
   
 interpretation "Nat modulus" 'modulus m n = (modulus m n).
+
+ndefinition divide_with_remainder ≝
+  λm, n: Nat.
+    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+(* Exponentials, and square roots.                                            *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
+
+nlet rec exponential (m: Nat) (n: Nat) on n ≝
+  match n with
+    [ Z ⇒ S (Z)
+    | S o ⇒ m * exponential m o
+    ].
+    
+notation "hvbox(n ^ m)"
+  left associative with precedence 52
+  for @{ 'exponential $n $m }.
+  
+interpretation "Nat exponential" 'exponential n m = (exponential n m).
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)