Zulip Chat Archive

Stream: general

Topic: simp not idempotent with `let`

Eric Rodriguez (Apr 06 2021 at 18:59):

Hey all! I've been trying to use a lot of lets in my code for clarity, but it feels like it always ends up being a pain to do so. For example, look at this mwe:

example : true :=
  let some_fun := λ asda : , ite (asda = 23  asda = 420) 123 456,
  suffices : some_fun 23 = some_fun 420, by trivial,
  simp [some_fun], simp,

For some reason, I need both simps; if I try just one, it pretty much just unfolds some_fun and then gives up. Is this something one of the hidden simp parameters can solve?

Last updated: Dec 20 2023 at 11:08 UTC