diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 8592e9af3a1b..786727f76c8b 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/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 diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 8e6ea4908324..032aae0e01df 100644 --- a/src/runtime/object.cpp +++ b/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);