Stream: Beginner Questions

Topic: Unfolding of let bindings

view this post on Zulip 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 *)

view this post on Zulip Mathias Fleury (Jan 03 2023 at 21:01):

You need to pass Let_def to the simplifier to get it unfolded

view this post on Zulip Hanno Becker (Jan 03 2023 at 21:09):

Oops. Thank you Mathias :-)

Last updated: Oct 13 2024 at 01:36 UTC