Changeset 273 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Nov 24, 2010, 2:28:34 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r271 r273 185 185 nqed. 186 186 187 ndefinition bitvector_of_nat ≝ 188 λm, n: Nat. 189 let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in 190 let size ≝ length Bool biglist in 191 let bitvector ≝ bitvector_of_list biglist in 192 let difference ≝ n  size in 193 pad difference size bitvector. 187 naxiom plus_minus_inverse_left: 188 ∀m, n: Nat. 189 (m + n)  n = m. 190 191 naxiom plus_minus_inverse_right: 192 ∀m, n: Nat. 193 (m  n) + n = m. 194 195 naxiom greater_than_b: Nat → Nat → Bool. 196 197 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝ 198 let biglist ≝ reverse ? (bitvector_of_nat_aux m) in 199 let size ≝ length ? biglist in 200 let bitvector ≝ bitvector_of_list biglist in 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. 210 nqed. 211 212 ncheck bitvector_of_nat. 194 213 195 214 nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
Note: See TracChangeset
for help on using the changeset viewer.