Theorem: Cpdt.Chapter2.TExp.compile_binop (Cpdt/Chapter2/Typed.lean)

State before:
r a✝ : Ty
op : TBinop a✝ r r
arg1 : TExp a✝
arg2 : TExp r
ts : TStack
⊢ compile (binop op arg1 arg2) ts = concat (compile arg2 ts) (concat (compile arg1 (r :: ts)) (cons (iBinop op) nil))
Tactic:
rfl
State after:
no goals