## 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 :=
begin
let some_fun := λ asda : ℕ, ite (asda = 23 ∨ asda = 420) 123 456,
suffices : some_fun 23 = some_fun 420, by trivial,
simp [some_fun], simp,
end


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: May 13 2021 at 22:15 UTC