Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: Capturing metavariable assignment
Jannis Limperg (May 11 2021 at 12:58):
For the proof search tactic I'm writing, I'd like to be able to capture and restore the current metavariable assignment. Specifically, I want to apply a tactic to a goal, do something with the produced subgoals, then later on backtrack to the state before the tactic was run. This backtracking should reset not only the goals but also any metavariables that were assigned by the tactic. Can I achieve this by just saving the tactic_state
?
Gabriel Ebner (May 11 2021 at 12:59):
Yes.
Jannis Limperg (May 11 2021 at 13:01):
Wonderful, thanks!
Last updated: Dec 20 2023 at 11:08 UTC