Lean.Elab.Tactic.run but with multiple goals

Stream: Is there code for X?

[Joachim Breitner]

docs#Lean.Elab.Tactic.run has type

Lean.MVarId → Lean.Elab.Tactic.TacticM Unit → Lean.Elab.TermElabM (List Lean.MVarId)

so you can use it to apply tactics to a single goal. It’s implementation has

     aux.runCore' { elaborator := .anonymous } { goals := [mvarId] }

so there clearly is a concept of “many goals”.

I can’t find a similar function for applying a tactic to many goal (so that they can for example be individually focused using \. or \case). Did I just not find it?

[Jannis Limperg]

You can always setGoals within the TacticM computation passed to run.

[Joachim Breitner]

Ah, ok. In that case, can I start TacticM without a MVar? What is the significance of this “first” MVar? It seems it somehow affects the context:

  mvarId.withContext do

(I guess I can try to use the first in my list, or create a throw-away MVar from TermElabM, but that’d just be guessing.)

[Kyle Miller]

I think that line is just making sure the local context is set to something reasonable. You could probably refactor Tactic.run to have a Tactic.runWith that takes a list of metavariables, and define

def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) :=
  mvarId.withContext do runWith [mvarId]

to preserve its current behavior