wrapSimpDischarger

Mathlib.Util.DischargerAsTactic

URI: https://scilib.ai/kg/mathlib#wrapSimpDischarger

Lean4

/-- Wrap a simp discharger (a function `Expr → SimpM (Option Expr)`) as a tactic,
so that it can be passed as an argument to `simp (discharger := foo)`.
This is inverse to `mkDischargeWrapper`. -/
def wrapSimpDischarger (dis : Simp.Discharge) : TacticM Unit := do
  let eS : Lean.Meta.Simp.State := { }
  let eC : Lean.Meta.Simp.Context := ← Simp.mkContext { }
  let eM : Lean.Meta.Simp.Methods := { }
  let (some a, _) ← liftM <| StateRefT'.run (ReaderT.run (ReaderT.run (dis <| ← getMainTarget) eM.toMethodsRef) eC) eS |
    failure
  (← getMainGoal).assignIfDefEq a

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

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

Разделы

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

Аффилиация

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