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.