fix: change 0 and 1 to false and true

src/Init/Data/ByteArray/Basic.lean

@@ -23,10 +23,18 @@ attribute [extern "lean_byte_array_data"] ByteArray.data
 
 namespace ByteArray
 
-deriving instance BEq for ByteArray
-
 attribute [ext] ByteArray
 
+/--
+Checks whether two `ByteArray` instances have the same length and identical content. Normally used
+via the `==` operator.
+-/
+@[extern "lean_byte_array_beq"]
+protected def beq (a b : @& ByteArray) : Bool :=
+  BEq.beq a.data b.data
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
 instance : DecidableEq ByteArray :=
   fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
 

src/runtime/object.cpp

@@ -2419,6 +2419,21 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_mk(obj_arg a) {
     return r;
 }
 
+extern "C" LEAN_EXPORT bool lean_byte_array_beq(obj_arg a, obj_arg b) {
+    if (a == b) {
+        return true;
+    }
+
+    size_t size_a = lean_sarray_size(a);
+    size_t size_b = lean_sarray_size(b);
+
+    if (size_a != size_b) {
+        return false;
+    }
+
+    return memcmp(lean_sarray_cptr(a), lean_sarray_cptr(b), size_a) == 0;
+}
+
 extern "C" LEAN_EXPORT obj_res lean_byte_array_data(obj_arg a) {
     usize sz       = lean_sarray_size(a);
     obj_res r      = lean_alloc_array(sz, sz);