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

Last change on this file since 228 was 228, checked in by mulligan, 10 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.