I wonder what the best way is to change the goal with something convertible. All I came up with is:
Ltac2 change_goal (new_goal : constr) := ltac1:( a b |- change a with b ) (Ltac1.of_constr (Control.goal())) (Ltac1.of_constr new_goal).
As discussed the Ltac2 change doesn't work for me because the "from term" is a pattern and not a constr. But maybe there is a way to replace the complete goal.
Ltac2 change_goal (new_goal : constr) := ltac1:( b |- change b ) (Ltac1.of_constr new_goal).
@Gaëtan Gilbert : thanks - I didn't use change without
with so far. But you also don't see a way around Ltac1?
@Pierre-Marie Pédrot once explained that change takes a pattern and that there is a rather obscure function to convert a term to a pattern. I wonder why there is no simple change function which changes a term with a term.
change with are actually pretty different tactics. There are no patterns involved in the former.
I checked and indeed it works as expected:
Ltac2 changef x := change $x. Goal True. changef constr:(id True).
change $new_goal works as expected! Thanks for point this out - as usual it is obvious once one knows it. I guess my main problem was that I didn't know a change without
with existed at all.
Last updated: May 31 2023 at 02:31 UTC