Changeset 2782 for src/ASM/BitVector.ma
- Timestamp:
- Mar 6, 2013, 3:03:02 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVector.ma
r2645 r2782 58 58 λm, n: nat. 59 59 λb: BitVector n. pad_vector ? false m n b. 60 61 (* jpb: we already have bitvector_of_nat and friends in the library, maybe62 * we should unify this in some way *)63 let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝64 match n with65 [ O ⇒ VEmpty ?66 | S n' ⇒67 eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)68 ].69 70 let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝71 match b with72 [ VEmpty ⇒ 073 | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].74 60 75 61 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset
for help on using the changeset viewer.