runTactic

Mathlib.Lean.ContextInfo

URI: https://scilib.ai/kg/mathlib#Lean.Elab.ContextInfo.runTactic

Lean4

/-- Run a tactic computation in the context of an infotree node. -/
def runTactic (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (x : MVarId → MetaM α) : CommandElabM α := do
  if !i.goalsBefore.contains goal then
    panic! "ContextInfo.runTactic: `goal` must be an element of `i.goalsBefore`"
  let mctx := i.mctxBefore
  let lctx := (mctx.decls.find! goal).2
  ctx.runMetaMWithMessages lctx <| do
      -- Make a fresh metavariable because the original goal is already assigned.

      let type ← goal.getType
      let goal ← Meta.mkFreshExprSyntheticOpaqueMVar type
      x goal.mvarId!

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru