Changeset 234 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 12, 2010, 2:27:56 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVector.ma
r232 r234 1 include "List.ma". 1 2 include "Vector.ma". 2 3 include "Nat.ma". … … 31 32 λc: BitVector n. 32 33 zip Bool Bool Bool n exclusive_disjunction b c. 34 35 ndefinition complement ≝ 36 λn: Nat. 37 λb: BitVector n. 38 map Bool Bool n (negation) b. 33 39 34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝ 35 match m with 36 [ Z ⇒ ? 37 | S o ⇒ ? 38 ]. 39 40 //. 41 nqed. 40 ndefinition divide_with_remainder ≝ 41 λm, n: Nat. 42 mk_Cartesian Nat Nat (m ÷ n) (modulus m n). 42 43 43 ncheck pad. 44 44 nlet rec bitvector_of_nat_aux (n: Nat): List Nat ≝ 45 let div_rem ≝ divide_with_remainder n (S (S Z)) in 46 let div ≝ first Nat Nat div_rem in 47 let rem ≝ second Nat Nat div_rem in 48 Empty Nat.
Note: See TracChangeset
for help on using the changeset viewer.