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
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):
I guess I never tried precisely this, but only
Last updated: May 12 2021 at 04:19 UTC