withRecurse

Mathlib.Tactic.GeneralizeProofs

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.GeneralizeProofs.MAbs.withRecurse

Lean4

/-- Runs `x` with an increased recursion depth and the initial local context, clearing `fvars`. -/
def withRecurse {α : Type} (x : MAbs α) : MAbs α := do
  withLCtx (← read).initLCtx (← getLocalInstances) do
      withReader (fun r => { r with fvars := #[], depth := r.depth + 1 }) x

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

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

Разделы

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

Аффилиация

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