12.1. Setup: Register Arguments

First, define register operands for the macro:

open X86.Examples  -- provides eax, ebx, ecx, edx, imm

Or define them yourself:

def eax : InstrArg := .Reg32 EAX
def imm (n : Nat) : InstrArg := .Imm32 (BitVec.ofNat 32 n)