Hanno Becker (Jan 20 2023 at 17:50): Hanno Becker (Jan 20 2023 at 17:50):Hi! I'm working with a fairly complex and time-consuming tactic for which I would like to avoid unnecessary invocations -- that is, invocations on subgoals on which the tactic has already been tried before. Has this been implemented before?
Implementing this in ML should be possible albeit a bit painful due to the need to remember state in case of failure (that's the point), but I'd like to avoid it if I can :-)
(By default, the tactic will be attempted on the first subgoal, upon failure the second, upon failure the third, etc. -- and if any goal could be progressed, the whole cycle will restart. This is necessary since, sometimes, a subgoal can only be progressed after instantiating a schematic that is shared with another subgoal which _can_ be progressed. At the minimum, I want to refine the criterion for doing another "loop" to "some schematic has been instantiated"; however, for subsequent top-level invocations of the method, a more general memory of what has already been tried would be more useful).
Last updated: Dec 21 2024 at 16:20 UTC