Stream: new members
Rui Liu (Dec 12 2020 at 15:17):
I want to perform reduction to a sub expression of the goal (or maybe any hypothesis in context), how do I do it?
Rui Liu (Dec 12 2020 at 15:18):
unfold doesn't seem to be what I want since it only unfolds definition? But I want to perform a reduction
Mario Carneiro (Dec 12 2020 at 15:32):
dsimp only often works
Rui Liu (Dec 12 2020 at 15:36):
Do I need to tag definitions as
simp somehow to get it working?
Kevin Buzzard (Dec 12 2020 at 15:38):
do you want to unfold definitions or don't you? :-) There are several ways you can deal with definitions -- you can make them
[reducible] or even abbreviations, or unfold them, and it wouldn't surprise me if you can tag them with simp as well if you want simp to do the job.
Rui Liu (Dec 12 2020 at 15:40):
How do I make sure unfold also does a reduction. Sometimes it seems unfold will just unfold the function, instead of applying it?
Johan Commelin (Dec 12 2020 at 15:40):
Adam Topaz (Dec 12 2020 at 15:41):
foo is the name of the definition)
Rui Liu (Dec 12 2020 at 16:43):
OK I seem to be able to proceed further with this
Last updated: May 14 2021 at 05:20 UTC