Hi all. Can someone explain why the
let binding is not unfolded by
auto in the following example?
lemma ‹f (let r = x y in g (λ_. t r r)) = f (g (λ_. t (x y) (x y)))› by auto (* FAIL *) by metis (* OK *)
You need to pass
Let_def to the simplifier to get it unfolded
Oops. Thank you Mathias :-)
Last updated: Dec 07 2023 at 20:16 UTC