Changeset 228 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Nov 9, 2010, 3:27:30 PM (11 years ago)
 File:

 1 moved
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r224 r228 1 include "Vectors.ma". 1 include "Vector.ma". 2 include "Nat.ma". 3 include "Bool.ma". 2 4 3 include "arithmetics/nat.ma". 4 include "basics/bool.ma". 5 ndefinition BitVector ≝ λn: Nat. Vector Bool n. 5 6 6 ndefinition BitVector ≝ λn: nat. Vector bool n. 7 7 ndefinition zero ≝ 8 λn: Nat. 9 replicate Bool n False. 10 8 11 ndefinition conjunction ≝ 9 λn: nat. 10 λv, q: BitVector n. 11 fold_right ∧ true v q. 12 λn: Nat. 13 λb: BitVector n. 14 λc: BitVector n. 15 zip Bool Bool Bool n conjunction b c. 16 17 ndefinition inclusive_disjunction ≝ 18 λn: Nat. 19 λb: BitVector n. 20 λc: BitVector n. 21 zip Bool Bool Bool n inclusive_disjunction b c. 22 23 ndefinition 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 TracChangeset
for help on using the changeset viewer.