name

Mathlib.Tactic.Have

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

Lean4

/-- Retrieves the name of the optional identifier, if provided. Returns `this` otherwise -/
def name (id : TSyntax ``optBinderIdent) : Name :=
  if id.raw[0].isIdent then id.raw[0].getId else HygieneInfo.mkIdent ⟨id.raw[0]⟩ `this |>.getId

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

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

Разделы

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

Аффилиация

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