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

Last change on this file since 232 was 232, checked in by mulligan, 10 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
Line 
1include "Vector.ma".
2include "Nat.ma".
3include "Bool.ma".
4
5ndefinition BitVector ≝ λn: Nat. Vector Bool n.
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)))))))))))))))).
11
12ndefinition zero ≝
13  λn: Nat.
14    replicate Bool n False.
15   
16ndefinition conjunction ≝
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.
32    zip Bool Bool Bool n exclusive_disjunction b c.
33
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.
44       
Note: See TracBrowser for help on using the repository browser.