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

Timestamp:

Nov 12, 2010, 2:27:56 PM (11 years ago)

Author:

mulligan

Message:

Division and modulus implemented. All necessary orders on naturals
completed. More operations on bitvectors (and general operations that
apply to all vectors) implemented.

File:

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

Deliverables/D4.1/Matita/BitVector.ma

@@ +1 @@
+include "List.ma".
 include "Vector.ma".
 include "Nat.ma".
@@ -31 +32 @@
   λc: BitVector n.
     zip Bool Bool Bool n exclusive_disjunction b c.
+    
+ndefinition complement ≝
+  λn: Nat.
+  λb: BitVector n.
+    map Bool Bool n (negation) b.
 
-nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝
-  match m with
-    [ Z ⇒ ?
-    | S o ⇒ ?
-    ].
-    
-    //.
-nqed.
+ndefinition divide_with_remainder ≝
+  λm, n: Nat.
+    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
 
-ncheck pad.
-        
+nlet rec bitvector_of_nat_aux (n: Nat): List Nat ≝
+  let div_rem ≝ divide_with_remainder n (S (S Z)) in
+  let div ≝ first Nat Nat div_rem in
+  let rem ≝ second Nat Nat div_rem in
+    Empty Nat.