Changeset 224 for Deliverables/D4.1/Matita/BitVectors.ma
- Timestamp:
- Nov 8, 2010, 5:04:27 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVectors.ma
r223 r224 1 include "Vectors.ma". 2 3 include "arithmetics/nat.ma". 4 include "basics/bool.ma". 5 6 ndefinition BitVector ≝ λn: nat. Vector bool n. 7 8 ndefinition conjunction ≝ 9 λn: nat. 10 λv, q: BitVector n. 11 fold_right ∧ true v q.
Note: See TracChangeset
for help on using the changeset viewer.