fact: Fixpoint eval {A} (s : store) (e : expr A) : tyeval A := match e with | Var n => s n | Plus e1 e2 => eval s e1 + eval s e2 | Equal e1 e2 => eval s e1 =? eval s e2 | Pair e1 e2 => (eval s e1, eval s e2) | Fst e => fst (eval s e) | Snd e => snd (eval s e) | Const _ c => c | Ite b e1 e2 => if eval s b then eval s e1 else eval s e2 end.
imports: Hammer(Tactics) Program.Equality Arith String