Targeted Reduce and Unfold
Opened this issue · 1 comments
jozefg commented
Currently reduce and Unfold globally apply their transformations. Instead they should be able to optionally take a path (for example, [h. =(foo; bar; h)]) and then only apply their transformations at that spot.
jonsterling commented
👍 Additionally, it should be possible to specify a target such that it only rewrites in a certain hypothesis, or in the conclusion, etc.