Zulip Chat Archive

Stream: general

Topic: unfold local definitions


Reid Barton (May 10 2018 at 16:35):

Is there a way in tactic mode to unfold something bound by a surrounding let?

Reid Barton (May 10 2018 at 16:45):

I guess I also want to do a beta reduction, since the thing I want to unfold is a function whose definition is assume x, ...

Gabriel Ebner (May 10 2018 at 16:50):

You can do dsimp [x] if x is the let-binding in the local context.

Gabriel Ebner (May 10 2018 at 16:51):

example : let x := 5 in x + x > 0 :=
begin
intro x,
dsimp [x],
-- 5 + 5 > 0
end

Reid Barton (May 10 2018 at 17:36):

Oh. Thanks!
I guess I never tried precisely this, but only unfold and rw.


Last updated: Dec 20 2023 at 11:08 UTC