BEq for ByteArray

Stream: lean4

[Arthur Paulino]

Is there a reason why BEq isn't implemented for ByteArray? There's a fast implementation possible in C with memcmp

[Arthur Paulino]

Would such an implementation be welcome in Batteries?

[François G. Dorais]

Lean4 would be the better place for an optimized implementation. However, revamping scalar arrays is a low priority TODO item that keeps popping up every so often. So the answer may well be to put it in that boat.

Batteries would accept it. Maintenance costs for C code is higher so we try to avoid it but this is a simple case so I don't see any major issues. Do get in contact with the maintainers ahead of time so we can coordinate how to arrange the C code.

[François G. Dorais]

I added a temporary and inefficient DecidableEq instance for ByteArray as part of batteries#1116