Hello,
I have a tactic, lets call it branch
which creates, some number of goals. I have another tactic, let’s call it solve
that solves the goal if there is enough information in the context. I want to apply combination of tactics in a depth-first manner. In other words, I want to branch
, then try solve
new goals, then branch
in first goal only. Do this recursively until that branch of goal tree is solved, then jump into the next first goal. How can I achieve this?