Theorem: Cpdt.Chapter2.Exp.compile_const (Cpdt/Chapter2/Lang.lean)

State before:
n : Nat
⊢ compile (const n) = [Instr.iConst n]
Tactic:
rfl
State after:
no goals