Changeset 271 for Deliverables/D4.1/Matita/BitVector.ma

Timestamp:

Nov 24, 2010, 1:00:41 AM (9 years ago)

Author:

sacerdot

Message:

assembly1 defined on ACALL and ADD: it seems it will become too slow...

File:

• Deliverables/D4.1/Matita/BitVector.ma (modified) (3 diffs)

Deliverables/D4.1/Matita/BitVector.ma

@@ -23 +23 @@
 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
-ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))).
+ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -200 +200 @@
         ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     ].
-    
+
+(*
 nlet rec equality (n: Nat) (b: BitVector n) (c: BitVector n) on b ≝
   match b with
@@ -209 +210 @@
     | Cons 
     ].
+*)