Changeset 2782 for src/ASM/BitVector.ma

Timestamp:

Mar 6, 2013, 3:03:02 AM (7 years ago)

Author:

sacerdot

Message:

1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the wrong indianess! removed
2. Dominic's nat_of_bitvector/bitvector_of_nat in Arithmetic.ma are inefficient. For the time being I have pasted there Paolo's code in a comment.

File:

• src/ASM/BitVector.ma (modified) (1 diff)

src/ASM/BitVector.ma

@@ -58 +58 @@
   λm, n: nat.
   λb: BitVector n. pad_vector ? false m n b.
-
-(* jpb: we already have bitvector_of_nat and friends in the library, maybe
- * we should unify this in some way *)  
-let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
-  match n with
-  [ O ⇒ VEmpty ?
-  | S n' ⇒
-    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
-  ].
-  
-let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
-  match b with
-  [ VEmpty ⇒ 0
-  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)