Changeset 2780 for extracted/bitVector.ml
 Timestamp:
 Mar 6, 2013, 2:59:22 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/bitVector.ml
r2773 r2780 65 65 Vector.pad_vector Bool.False m n b 66 66 67 (** val nat_to_bv : Nat.nat > Nat.nat > bitVector **)68 let rec nat_to_bv n k =69 match n with70  Nat.O > Vector.VEmpty71  Nat.S n' >72 Vector.VCons (n',73 (Nat.eqb (Util.modulus k (Nat.S (Nat.S Nat.O))) (Nat.S Nat.O)),74 (nat_to_bv n' (Util.division k (Nat.S (Nat.S Nat.O)))))75 76 (** val bv_to_nat : Nat.nat > bitVector > Nat.nat **)77 let rec bv_to_nat n = function78  Vector.VEmpty > Nat.O79  Vector.VCons (n', x, b') >80 Nat.plus81 (match x with82  Bool.True > Nat.S Nat.O83  Bool.False > Nat.O)84 (Nat.times (bv_to_nat n' b') (Nat.S (Nat.S Nat.O)))85 86 67 (** val conjunction_bv : Nat.nat > bitVector > bitVector > bitVector **) 87 68 let conjunction_bv n b c =
Note: See TracChangeset
for help on using the changeset viewer.