CoqToLeanAsm: x86 Macro Assembler in Lean 4

5.2. Operand Size Type

The OpSize type captures x86 operand sizes:

X86.OpSize.Op8 : OpSize#check OpSize.Op8 -- 8-bit operations X86.OpSize.Op16 : OpSize#check OpSize.Op16 -- 16-bit operations X86.OpSize.Op32 : OpSize#check OpSize.Op32 -- 32-bit operations (default in protected mode)

The VWord type family maps OpSize to BitVec:

VWord OpSize.Op32 : Type#check (VWord OpSize.Op32)