elab with tactics

Stream: lean4

[louq]

Im figuring out how to use elab

elab "process_all_goals" : tactic => do
  let goal_type ← Lean.Elab.Tactic.getMainTarget
  let glctx <- Lean.MonadLCtx.getLCtx

I want to use tactics during elaboration. Is there a way for this?

[Leni Aniva]

louq said:

Im figuring out how to use elab

elab "process_all_goals" : tactic => do
  let goal_type ← Lean.Elab.Tactic.getMainTarget
  let glctx <- Lean.MonadLCtx.getLCtx

I want to use tactics during elaboration. Is there a way for this?

you can run the TacticM monad inside of your Elab.TermM monad

let tacticM : TacticM := do
  ...
tacticM.run { elaborator := .anonymous } |>.run { goals := [goal] }

[louq]

can you give me an example

[Leni Aniva]

louq said:

can you give me an example

do you mean an example of running TacticM inside Elab.TermM?

[louq]

yes.

[Kyle Miller]

Maybe you're looking for docs#Lean.Elab.Tactic.evalTactic ?

If you want to construct a proof from a tactic script, you could also do elabTermEnsuringType (<- `(by my_tactics)) goal_type. That's docs#Lean.Elab.Tactic.elabTermEnsuringType

[Leni Aniva]

louq said:

yes.

def runTacticM (mvarId: MVarId) (tactic: Elab.Tactic.TacticM Unit): Elab.TermElabM (List MVarId) := do
  mvarId.checkNotAssigned `runTacticM
  let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] }
  return newGoals

like this?

[louq]

Leni Aniva said:

louq said:

yes.

def runTacticM (mvarId: MVarId) (tactic: Elab.Tactic.TacticM Unit): Elab.TermElabM (List MVarId) := do
  mvarId.checkNotAssigned `runTacticM
  let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] }
  return newGoals

like this?

Im using lean4 web version. Can you show me the use of this in lean4?