41 type bitVector = Bool.bool Vector.vector
45 type nibble = bitVector
47 type byte7 = bitVector
53 type word11 = bitVector
55 (** val zero : Nat.nat -> bitVector **)
57 Vector.replicate n Bool.False
59 (** val maximum : Nat.nat -> bitVector **)
61 Vector.replicate n Bool.True
63 (** val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector **)
65 Vector.pad_vector Bool.False m n b
67 (** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
68 let conjunction_bv n b c =
69 Vector.zip_with n Bool.andb b c
71 (** val inclusive_disjunction_bv :
72 Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
73 let inclusive_disjunction_bv n b c =
74 Vector.zip_with n Bool.orb b c
76 (** val exclusive_disjunction_bv :
77 Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
78 let exclusive_disjunction_bv n b c =
79 Vector.zip_with n Bool.xorb b c
81 (** val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector **)
83 Vector.map n Bool.notb b
85 (** val eq_b : Bool.bool -> Bool.bool -> Bool.bool **)
89 | Bool.False -> Bool.notb c
91 (** val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool **)
93 Vector.eq_v n eq_b b c
96 Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
97 let eq_bv_elim n x y ht hf =
98 Vector.eq_v_elim eq_b (fun _ clearme ->
103 | Bool.True -> (fun auto auto' -> auto __)
104 | Bool.False -> (fun auto auto' -> auto' __))
108 | Bool.True -> (fun auto auto' -> auto' __)
109 | Bool.False -> (fun auto auto' -> auto __))) n x y ht hf