CoqToLeanAsm: x86 Macro Assembler in Lean 4

6.3. Word Registers

16-bit registers via WordReg access the lower 16 bits:

X86.AX : WordReg#check AX -- Lower 16 bits of EAX X86.DX : WordReg#check DX -- Lower 16 bits of EDX