CoqToLeanAsm: x86 Macro Assembler in Lean 4

5.3. Byte Operations

X86.Byte.toHex (b : Byte) : String#check Byte.toHex -- Extract bytes from DWord (little-endian, index 0 = LSB) X86.DWord.toByte (d : DWord) (idx : Fin 4) : Byte#check DWord.toByte -- Construct DWord from bytes X86.DWord.fromBytes (b0 b1 b2 b3 : Byte) : DWord#check DWord.fromBytes