fact: Definition compile_bexp (symbols : list string) (b : bexpr0 string) : list assembly := match b with | blt e1 e2 => compile_aexp symbols e1 ++ compile_aexp symbols e2 ++ [cmp] end.
imports: ZArith Arith List syntax little Lia