Scott Morrison (Oct 03 2018 at 09:03):
Is there an existing tactic that runs a tactic, then restores the original tactic_state if it fails?
Patrick Massot (Oct 03 2018 at 09:04):
Scott Morrison (Oct 03 2018 at 09:04):
(I've run into a problem where failed tactics are having unwanted side effects, e.g. unifying metavariables.)
Simon Hudon (Oct 03 2018 at 09:24):
So you write
tac unifies variables and then fails and the unification persists?
Mario Carneiro (Oct 03 2018 at 09:28):
try definitely restores the original tactic state after failure, so it's possible you've stumbled upon one of lean's less functional sides
Scott Morrison (Oct 03 2018 at 09:31):
Hmm, it seems I was wrong, as sticking such a tactic into the place I thought would fix things, hasn't fixed things. Maybe more later, sorry for the noise!
Last updated: Aug 03 2023 at 10:10 UTC