runMAbs

Mathlib.Tactic.GeneralizeProofs

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.GeneralizeProofs.MGen.runMAbs

Lean4

/-- Runs `MAbs` in `MGen`. Returns the value and the `generalizations`. -/
def runMAbs {α : Type} (mx : MAbs α) : MGen (α × Array (Expr × Expr)) := do
  let s ← get
  let (x, s') ← mx |>.run { initLCtx := ← getLCtx, propToFVar := s.propToFVar, config := (← read) } |>.run |>.run { }
  return (x, s'.generalizations)

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

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

Разделы

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

Аффилиация

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