optBinderIdent

Mathlib.Tactic.Have

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.optBinderIdent

Lean4

/-- A parser for optional binder identifiers -/
def optBinderIdent : Parser :=
  leading_parser
    -- Note: the withResetCache is because leading_parser seems to add a cache boundary,
      -- which causes the `hygieneInfo` parser not to be able to undo the trailing whitespace
     (ppSpace >> Term.binderIdent) <|> withResetCache hygieneInfo

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

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

Разделы

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

Аффилиация

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