withLocal

Mathlib.Tactic.GeneralizeProofs

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

Lean4

/-- Runs `x` with an additional local variable. -/
def withLocal {α : Type} (fvar : Expr) (x : MAbs α) : MAbs α :=
  withReader (fun r => { r with fvars := r.fvars.push fvar }) x

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

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

Разделы

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

Аффилиация

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