matchVar

Mathlib.Util.Notation3

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

Lean4

/-- Matcher that assigns the current `SubExpr` into the match state;
if a value already exists, then it checks for equality. -/
def matchVar (c : Name) : Matcher := fun s => do
  if let some (se, _, _) := s.vars[c]? then
    guard <| se.expr == (← getExpr)
    return s
  else
    s.captureSubexpr c

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

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

Разделы

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

Аффилиация

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