Changeset 266 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 23, 2010, 5:10:40 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVector.ma
r263 r266 33 33 λb: BitVector n. 34 34 λm: Nat. 35 get_index Bool n b m. 35 λp: m < n. 36 get_index Bool n b m p. 36 37 37 38 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). … … 41 42 λb: BitVector n. 42 43 λm: Nat. 43 set_index_weak Bool n b m. 44 λp: m < n. 45 λc: Bool. 46 set_index_weak Bool n b m c. 44 47 45 48 ndefinition drop ≝
Note: See TracChangeset
for help on using the changeset viewer.