Open JamesGallicchio opened 6 months ago
See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Marshalling.20lean.20UInt*.20into.20byte.20arrays
I think the most sensible design is to add UInt*.BytesBE and UInt*.BytesLE wrapper structures, with UInt*.toBytes[BL]E functions. Then we can add Indexed instances on the wrapper structures, using Fin 2/4/8 as the index.
UInt*.BytesBE
UInt*.BytesLE
UInt*.toBytes[BL]E
Indexed
Fin 2/4/8
See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Marshalling.20lean.20UInt*.20into.20byte.20arrays
I think the most sensible design is to add
UInt*.BytesBEandUInt*.BytesLEwrapper structures, withUInt*.toBytes[BL]Efunctions. Then we can addIndexedinstances on the wrapper structures, usingFin 2/4/8as the index.