fact: Fixpoint compile_aexp (a: aexp) : code := match a with | CONST n => Iconst n :: nil | VAR x => Ivar x :: nil | PLUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iadd :: nil | MINUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ Iopp :: Iadd :: nil end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)