Changeset 1599 for src/utilities/binary

Timestamp:

Dec 13, 2011, 1:34:37 AM (10 years ago)

Author:

sacerdot

Message:

Start of merging of stuff into the standard library of Matita.

File:

• src/utilities/binary/division.ma (modified) (5 diffs)

src/utilities/binary/division.ma

@@ -50 +50 @@
   ]
 | p0 m' ⇒
-  match divide m' n with
-  [ pair q r ⇒
+  let 〈q,r〉 ≝ divide m' n in
     match r with
     [ pzero ⇒ 〈natp0 q,pzero〉
@@ -61 +60 @@
       ]
     ]
-  ]
 | p1 m' ⇒
-  match divide m' n with
-  [ pair q r ⇒
+  let 〈q,r〉 ≝ divide m' n in
     match r with
     [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
@@ -74 +71 @@
       ]
     ]
-  ]
 ].
 
@@ -326 +322 @@
     [ OZ ⇒ OZ
     | pos m ⇒ natp_to_Z (fst ?? (divide n m))
-    | neg m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
+    | neg m ⇒ let 〈q,r〉 ≝ divide n m in
+                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ]
     ]
   | neg n ⇒
     match y with
     [ OZ ⇒ OZ
-    | pos m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
+    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
+                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ]
     | neg m ⇒ natp_to_Z (fst ?? (divide n m))
     ]
@@ -345 +341 @@
     [ OZ ⇒ OZ
     | pos m ⇒ natp_to_Z (snd ?? (divide n m))
-    | neg m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
+    | neg m ⇒ let 〈q,r〉 ≝ divide n m in
+                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ]
     ]
   | neg n ⇒
     match y with
     [ OZ ⇒ OZ
-    | pos m ⇒ match divide n m with [ pair q r ⇒
-                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
+    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
+                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ]
     | neg m ⇒ natp_to_Z (snd ?? (divide n m))
     ]