Changeset 351 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Dec 1, 2010, 4:30:46 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r349 r351 200 200 let bitvector ≝ bitvector_of_list biglist in 201 201 let difference ≝ n  size in 202 match greater_than_b size n with 203 [ true ⇒ max n 204  false ⇒ ? (pad difference size bitvector) 205 ]. 206 nnormalize. 207 nrewrite > (plus_minus_inverse_right n ?). 208 #H. 209 nassumption. 202 less_than_or_equal_b_elim … 203 (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉)) 204 (λH:¬(size ≤ n). max n). 205 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption. 210 206 nqed. 211 207
Note: See TracChangeset
for help on using the changeset viewer.