Changeset 337 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Nov 30, 2010, 12:26:45 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r330 r337 29 29 (* ===================================== *) 30 30 31 ndefinition get_index ≝31 ndefinition get_index_bv ≝ 32 32 λn: Nat. 33 33 λb: BitVector n. … … 38 38 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). 39 39 40 ndefinition set_index ≝40 ndefinition set_index_bv ≝ 41 41 λn: Nat. 42 42 λb: BitVector n. … … 120 120 'exclusive_disjunction b c = (exclusive_disjunction ? b c). 121 121 122 ndefinition negation ≝122 ndefinition negation_bv ≝ 123 123 λn: Nat. 124 124 λb: BitVector n. … … 131 131 (* ===================================== *) 132 132 133 ndefinition rotate_left ≝134 λ m, n: Nat.133 ndefinition rotate_left_bv ≝ 134 λn, m: Nat. 135 135 λb: BitVector n. 136 136 rotate_left Bool n m b. 137 137 138 ndefinition rotate_right ≝139 λ m, n: Nat.138 ndefinition rotate_right_bv ≝ 139 λn, m: Nat. 140 140 λb: BitVector n. 141 141 rotate_right Bool n m b. 142 142 143 ndefinition shift_left ≝144 λ m, n: Nat.143 ndefinition shift_left_bv ≝ 144 λn, m: Nat. 145 145 λb: BitVector n. 146 146 λc: Bool. 147 147 shift_left Bool n m b c. 148 148 149 ndefinition shift_right ≝150 λ m, n: Nat.149 ndefinition shift_right_bv ≝ 150 λn, m: Nat. 151 151 λb: BitVector n. 152 152 λc: Bool.
Note: See TracChangeset
for help on using the changeset viewer.