Zulip Chat Archive

Stream: general

Topic: discard tactic_state after failure?

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 try tac, 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: Dec 20 2023 at 11:08 UTC