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

Timestamp:

Nov 22, 2010, 11:43:04 AM (10 years ago)

Author:

mulligan

Message:

More changes. Added datatype for addressing modes.

File:

• Deliverables/D4.1/Matita/BitVector.ma (modified) (2 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))))))))))))).
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -196 +197 @@
     | Cons o hd tl ⇒
       let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
-        ((exponential (S (S Z)) o) × hdval) + nat_of_bitvector o tl
+        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     ].