Changeset 2782 for src/ASM/Arithmetic.ma
 Timestamp:
 Mar 6, 2013, 3:03:02 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2700 r2782 145 145 \fst (sub_with_borrows n b (zero n) true). 146 146 147 (* The following implementation is extremely inefficient*) 147 148 let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝ 148 149 match m with … … 153 154 definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝ 154 155 λn,m. bitvector_of_nat_aux n m (zero n). 156 157 (* This one by Paolo is efficient, but it is for the opposite indianess. 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  167 let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝ 168  match b with 169  [ VEmpty ⇒ 0 170   VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2]. 171  172 *) 155 173 156 174 let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
Note: See TracChangeset
for help on using the changeset viewer.