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

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

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 602 bytes
Line 
1include "Vector.ma".
2include "Nat.ma".
3include "Bool.ma".
4
5ndefinition BitVector ≝ λn: Nat. Vector Bool n.
6
7ndefinition zero ≝
8  λn: Nat.
9    replicate Bool n False.
10   
11ndefinition conjunction ≝
12  λn: Nat.
13  λb: BitVector n.
14  λc: BitVector n.
15    zip Bool Bool Bool n conjunction b c.
16   
17ndefinition inclusive_disjunction ≝
18  λn: Nat.
19  λb: BitVector n.
20  λc: BitVector n.
21    zip Bool Bool Bool n inclusive_disjunction b c.
22   
23ndefinition exclusive_disjunction ≝
24  λn: Nat.
25  λb: BitVector n.
26  λc: BitVector n.
27    zip Bool Bool Bool n exclusive_disjunction b c.
28   
29   
Note: See TracBrowser for help on using the repository browser.