Lean4
/-- `extractCtxAndGoals take? tree` takes as input a function `take? : Syntax → Bool` and
an `InfoTree` and returns the array of pairs `(stx, mvars)`,
where `stx` is a syntax node such that `take? stx` is `true` and
`mvars` indicates the goal state:
* the context before `stx`
* the context after `stx`
* a list of metavariables closed by `stx`
* a list of metavariables created by `stx`
A typical usage is to find the goals following a `simp` application.
-/
partial def extractCtxAndGoals : InfoTree → Array (Syntax × MetavarContext × MetavarContext × List MVarId × List MVarId)
| .node k args =>
let kargs := (args.map extractCtxAndGoals).foldl (· ++ ·) #[]
if let .ofTacticInfo i := k then
if take? i.stx && (i.stx.getRange? true).isSome then
#[(i.stx, i.mctxBefore, i.mctxAfter, i.goalsTargetedBy, i.goalsCreatedBy)] ++ kargs
else kargs
else kargs
| .context _ t => extractCtxAndGoals t
| _ => default
