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
RevLine 
[228]1include "Vector.ma".
2include "Nat.ma".
3include "Bool.ma".
[224]4
[228]5ndefinition BitVector ≝ λn: Nat. Vector Bool n.
[224]6
[228]7ndefinition zero ≝
8  λn: Nat.
9    replicate Bool n False.
10   
[224]11ndefinition conjunction ≝
[228]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.