Changeset 315 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Nov 26, 2010, 5:32:34 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r314 r315 185 185 nqed. 186 186 187 ndefinition eq_bv ≝ 188 λn: Nat. 189 λb, c: BitVector n. 190 eq_v Bool n (λd, e. 191 if inclusive_disjunction (conjunction d e) (conjunction (negation d) 192 (negation e)) then 193 true 194 else 195 false) b c. 196 187 197 naxiom plus_minus_inverse_left: 188 198 ∀m, n: Nat.
Note: See TracChangeset
for help on using the changeset viewer.