module CoqBvector: sig .. end
Implementing Coq's Bvector type conservatively with int64
type 'a bvector = int64
exception Overflow
val xO : 'a bvector -> 'a bvector
val xI : 'a bvector -> 'a bvector
val plus : 'a bvector -> 'a bvector -> 'a bvector
val minus : 'a bvector -> 'a bvector -> 'a bvector
val times : 'a bvector -> 'a bvector -> 'a bvector
val inc : CoqNat.nat -> 'a bvector -> 'a bvector
val dec : CoqNat.nat -> 'a bvector -> 'a bvector
val bvec_to_nat : CoqNat.nat -> 'a bvector -> CoqNat.nat
val nat_to_bvec : CoqNat.nat -> CoqNat.nat -> 'a bvector
val bvec_eq_dec : CoqNat.nat -> 'a bvector -> 'a bvector -> bool
val bneg : CoqNat.nat -> 'a bvector -> 'a bvector
val bVand : CoqNat.nat ->
'a bvector -> 'a bvector -> 'a bvector
val bVor : CoqNat.nat ->
'a bvector -> 'a bvector -> 'a bvector