Lean4
/-- `getManyGoals t` returns the syntax nodes of the `InfoTree` `t` corresponding to tactic calls
which
* leave at least one goal that was present before it ran
(with the exception of tactics that leave the sole goal unchanged);
* are not excluded through `exclusions` or `ignoreBranch`;
together with the number of goals before the tactic,
the number of goals after the tactic, and the number of unaffected goals.
-/
partial def getManyGoals : InfoTree → Array (Syntax × Nat × Nat × Nat)
| .node info args =>
let kargs := (args.map getManyGoals).toArray.flatten
if let .ofTacticInfo info := info then
if ignoreBranch.contains info.stx.getKind then
#[]
-- Ideal case: one goal, and it might or might not be closed.
else
if info.goalsBefore.length == 1 && info.goalsAfter.length ≤ 1 then kargs
else
if let .original .. := info.stx.getHeadInfo then
let backgroundGoals := info.goalsAfter.filter (info.goalsBefore.contains ·)
if backgroundGoals.length != 0 && !exclusions.contains info.stx.getKind then
kargs.push (info.stx, info.goalsBefore.length, info.goalsAfter.length, backgroundGoals.length)
else kargs
else kargs
else kargs
| .context _ t => getManyGoals t
| _ => default
