fact: Fixpoint cfold t (e : exp' t) : exp' t := match e with | NConst n => NConst n | Plus e1 e2 => let e1' := cfold e1 in let e2' := cfold e2 in match e1', e2' return exp' Nat with | NConst n1, NConst n2 => NConst (n1 + n2) | _, _ => Plus e1' e2' end | Eq e1 e2 => let e1' := cfold e1 in let e2' := cfold e2 in match e1', e2' return exp' Bool with | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false) | _, _ => Eq e1' e2' end | BConst b => BConst b | Cond n tests bodies default => cfoldCond (cfold default) (fun idx => cfold (tests idx)) (fun idx => cfold (bodies idx)) end.
imports: Arith List Program Equations.Prop.Equations