CoqToLeanAsm: x86 Macro Assembler in Lean 4

9.2. ifThenElse

Generates conditional branching:

X86.ifThenElse (cc : Condition) (cv : Bool) (pthen pelse : ProgBuilder Unit) : ProgBuilder Unit#check ifThenElse X86.ifThen (cc : Condition) (cv : Bool) (pthen : ProgBuilder Unit) : ProgBuilder Unit#check ifThen

Pattern:

  ; test (sets flags)
  Jcc else_label
  ; then code
  JMP end_label
else_label:
  ; else code
end_label: