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

Timestamp:

Nov 23, 2010, 2:30:10 PM (9 years ago)

Author:

sacerdot

Message:

• Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
• ambiguity reduced by lower-casing booleans

File:

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

Deliverables/D4.1/Matita/BitVector.ma

@@ -55 +55 @@
 ndefinition zero ≝
   λn: Nat.
-    ((replicate Bool n False): BitVector n).
+    ((replicate Bool n false): BitVector n).
     
 ndefinition max ≝
   λn: Nat.
-    ((replicate Bool n True): BitVector n).
+    ((replicate Bool n true): BitVector n).
     
 ndefinition append ≝
@@ -72 +72 @@
   λm, n: Nat.
   λb: BitVector n.
-    let padding ≝ replicate Bool m False in
+    let padding ≝ replicate Bool m false in
       append Bool m n padding b.
       
@@ -173 +173 @@
         match rem with
           [ Z ⇒ Empty Bool
-          | S r ⇒ ? (True :: (bitvector_of_nat_aux Z))
+          | S r ⇒ ? (true :: (bitvector_of_nat_aux Z))
           ]
       | S d ⇒
         match rem with
-          [ Z ⇒ ? (False :: (bitvector_of_nat_aux (S d)))
-          | S r ⇒ ? (True :: (bitvector_of_nat_aux (S d)))
+          [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d)))
+          | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d)))
           ]
       ].
@@ -196 +196 @@
     [ Empty ⇒ Z
     | Cons o hd tl ⇒
-      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
+      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
         ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     ].