withVar

Mathlib.Util.Notation3

URI: https://scilib.ai/kg/mathlib#Mathlib.Notation3.MatchState.withVar

Lean4

/-- Evaluate `f` with the given variable's value as the `SubExpr` and within that subexpression's
saved context. Fails if the variable has no value. -/
def withVar {α : Type} (s : MatchState) (name : Name) (m : DelabM α) : DelabM α := do
  let some (se, lctx, linsts) := s.vars[name]? |
    failure
  withLCtx lctx linsts <| withTheReader SubExpr (fun _ => se) <| m

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

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

Разделы

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

Аффилиация

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