source: Deliverables/D4.1/Matita/ @ 231

Last change on this file since 231 was 231, checked in by mulligan, 11 years ago

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File size: 998 bytes
1include "".
2include "".
3include "".
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)))))))))))))))).
12ndefinition zero ≝
13  λn: Nat.
14    replicate Bool n False.
16ndefinition conjunction ≝
17  λn: Nat.
18  λb: BitVector n.
19  λc: BitVector n.
20    zip Bool Bool Bool n conjunction b c.
22ndefinition inclusive_disjunction ≝
23  λn: Nat.
24  λb: BitVector n.
25  λc: BitVector n.
26    zip Bool Bool Bool n inclusive_disjunction b c.
28ndefinition exclusive_disjunction ≝
29  λn: Nat.
30  λb: BitVector n.
31  λc: BitVector n.
32    zip Bool Bool Bool n exclusive_disjunction b c.
34nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝
Note: See TracBrowser for help on using the repository browser.