Marshalling lean UInt* into byte arrays

Stream: lean4

[Siddharth Bhat]

I'm starting to write this type of code again, that converts a UInt* into a ByteArray and/or writes it out into a file for marshalling things like ELF and WAV files. What's the correct place for me to PR this? I assume it is std? I'm happy to put up a quick PR that takes a UInt* and produces a ByteArray. I imagine that longer term there's going to be a serde equivalent?

[Kim Morrison]

Isn't (x &&& 0xff).toUInt8 the same as x.toUInt8?

[Kim Morrison]

I'm not sure what you're proposing PRing. Functions UInt*.toByteArray? A class ToByteArray and instances for UInt*?

[Kim Morrison]

Could this just start off as its own repo?

[Timo Carlin-Burns]

I think UInt*.to{Be,Le,Ne}Bytes should be welcome in Std. Rust has them