Hanno Becker (Jan 03 2023 at 20:37): Hanno Becker (Jan 03 2023 at 20:37):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
Hanno Becker (Jan 03 2023 at 21:09):Oops. Thank you Mathias :-)
Last updated: Dec 21 2024 at 16:20 UTC