source: Deliverables/D4.1/Matita/BitVector.ma @ 232

Last change on this file since 232 was 232, checked in by mulligan, 9 years ago

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

File size: 1.1 KB
RevLine 
[228]1include "Vector.ma".
2include "Nat.ma".
3include "Bool.ma".
[224]4
[228]5ndefinition BitVector ≝ λn: Nat. Vector Bool n.
[230]6ndefinition Bit ≝ BitVector (S Z).
7ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
8ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
9ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
10ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
[224]11
[228]12ndefinition zero ≝
13  λn: Nat.
14    replicate Bool n False.
15   
[224]16ndefinition conjunction ≝
[228]17  λn: Nat.
18  λb: BitVector n.
19  λc: BitVector n.
20    zip Bool Bool Bool n conjunction b c.
21   
22ndefinition inclusive_disjunction ≝
23  λn: Nat.
24  λb: BitVector n.
25  λc: BitVector n.
26    zip Bool Bool Bool n inclusive_disjunction b c.
27   
28ndefinition exclusive_disjunction ≝
29  λn: Nat.
30  λb: BitVector n.
31  λc: BitVector n.
[231]32    zip Bool Bool Bool n exclusive_disjunction b c.
33
[232]34nlet 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    //.
41nqed.
42
43ncheck pad.
[231]44       
Note: See TracBrowser for help on using the repository browser.