diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
index 24d4d1b90..7e2d7f2e7 100644
--- a/test/lean/bitvec_operation.expected.lean
+++ b/test/lean/bitvec_operation.expected.lean
@@ -1,3 +1,9 @@
+def bitvector_eq (x : BitVec 16) (y : BitVec 16) : Bool :=
+  (Eq x y)
+
+def bitvector_neq (x : BitVec 16) (y : BitVec 16) : Bool :=
+  (Ne x y)
+
 def bitvector_append (x : BitVec 16) (y : BitVec 16) : BitVec 32 :=
   (BitVec.append x y)
 
diff --git a/test/lean/bitvec_operation.sail b/test/lean/bitvec_operation.sail
index 24de92c3e..a8b6861cb 100644
--- a/test/lean/bitvec_operation.sail
+++ b/test/lean/bitvec_operation.sail
@@ -2,6 +2,16 @@ default Order dec
 
 $include <prelude.sail>
 
+val bitvector_eq : (bits(16), bits(16)) -> bool
+function bitvector_eq(x, y) = {
+  x == y
+}
+
+val bitvector_neq : (bits(16), bits(16)) -> bool
+function bitvector_neq(x, y) = {
+  x != y
+}
+
 val bitvector_append : (bits(16), bits(16)) -> bits(32)
 function bitvector_append(x, y) = {
   append (x, y)