fact: Fixpoint ab_eval (g:string->Ab.t) (e: aexpr) {struct e}: Ab.t := match e with anum n => Ab.of_int n | avar x => g x | aplus e1 e2 => Ab.plus (ab_eval g e1)(ab_eval g e2) end.
imports: syntax little denot Bool List String ZArith axiom