Changeset 238 for Deliverables/D4.1/Matita/BitVector.ma
- Timestamp:
- Nov 12, 2010, 5:09:39 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVector.ma
r237 r238 69 69 λb: BitVector n. 70 70 map Bool Bool n (negation) b. 71 72 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 73 (* Rotates and shifts. *) 74 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 75 76 ndefinition rotate_left ≝ 77 λm, n: Nat. 78 λb: BitVector n. 79 rotate_left Bool n m b. 80 81 ndefinition rotate_right ≝ 82 λm, n: Nat. 83 λb: BitVector n. 84 rotate_right Bool n m b. 71 85 72 86 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset
for help on using the changeset viewer.