runTacticCode

Mathlib.Lean.ContextInfo

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

Lean4

/-- Run tactic code, given by a piece of syntax, in the context of an infotree node. -/
def runTacticCode (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (code : Syntax) : CommandElabM (List MVarId) :=
  do
  let termCtx ← liftTermElabM read
  let termState ← liftTermElabM get
  ctx.runTactic i goal fun goal => Lean.Elab.runTactic' (ctx := termCtx) (s := termState) goal code

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

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

Разделы

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

Аффилиация

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