RFC: byte(string) literals

Proposal

I propose the addition of a byte literal and bytestring literal syntax to Lean, in the spirit of Rust, so we can write patterns such as:

• '+'.toUInt8 as b'+' which would have type UInt8
• "hello".toUTF8 as b"hello" which would have type ByteArray
• support for raw byte string literals using br"hello" syntax for consistency with "normal" strings

In particular taking over the capability of Rust to support explicit byte escape syntax such as b"\x52" seems sensible to support as well.

Adding support for interpolated bytestring literals is out of scope for this RFC (and I don't think this should be supported).

The syntax b'+' should elaborate to the corresponding UInt8 literal 43 directly. The syntax b"hello" should elaborate to ByteArray.mk #[104, 101, 108, 108, 111]. Both of these should be represented in the simp normal form of their respective types such that simp doesn't mess up delaboration of these literals.

This will help users writing serializers/deserializers for both binary file formats as well as network protocols to write more succinct code. For examples of code that might benefit from this see https://github.com/leanprover/lean4/blob/master/src/Std/Tactic/BVDecide/LRAT/Parser.lean. Bytestring literals are going to end up being useful once we start implementing more advanced network protocols that communicate through longer strings of binary data.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

The only file mentioned is src/Std/Tactic/BVDecide/LRAT/Parser.lean, presented as an example of code that could benefit. Start by locating the language's literal syntax and elaboration entry points, then add coverage for b'...', b"...", br"...", explicit byte escapes, and simp/delaboration behavior; interpolation remains out of scope.