Michael Soegtrop (Nov 16 2022 at 19:17): Michael Soegtrop (Nov 16 2022 at 19:17):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.
Gaëtan Gilbert (Nov 16 2022 at 19:48):why not
Ltac2 change_goal (new_goal : constr) :=
ltac1:( b |- change b ) (Ltac1.of_constr new_goal).
?
Michael Soegtrop (Nov 17 2022 at 09:19):@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.
Pierre-Marie Pédrot (Nov 17 2022 at 09:28):change and change with are actually pretty different tactics. There are no patterns involved in the former.
Pierre-Marie Pédrot (Nov 17 2022 at 09:35):I checked and indeed it works as expected:
Ltac2 changef x := change $x.
Goal True.
changef constr:(id True).
Indeed simply 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: Apr 16 2024 at 15:02 UTC