 Timestamp:
 Mar 7, 2013, 12:10:42 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2782 r2796 157 157 (* This one by Paolo is efficient, but it is for the opposite indianess. 158 158 (* jpb: we already have bitvector_of_nat and friends in the library, maybe 159  * we should unify this in some way *) 160 let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝ 161  match n with 162  [ O ⇒ VEmpty ? 163   S n' ⇒ 164  eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2) 165  ]. 166  159  * we should unify this in some way *) 160 (* Paolo: converted to good endianness *) 161 let rec bitvector_of_nat_aux (n_acc : nat) (acc :BitVector n_acc) n (k : nat) on n : BitVector (plus n_acc n) ≝ 162 match n return λn.BitVector (plus n_acc n) with 163 [ O ⇒ acc⌈BitVector n_acc ↦ ?⌉ 164  S n' ⇒ 165 bitvector_of_nat_aux (S n_acc) (eqb (k mod 2) 1 ::: acc) n' (k ÷ 2) 166 ⌈BitVector (S n_acc + n') ↦ ?⌉ 167 ]. 168 [ cases (plus_n_O ?)  cases (plus_n_Sm ??) ] % qed. 169 170 definition bitvector_of_nat : ∀n.ℕ → BitVector n ≝ bitvector_of_nat_aux' ? [[ ]]. 171 167 172 let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝ 168 173  match b with
Note: See TracChangeset
for help on using the changeset viewer.