getAttrNames

Mathlib.Tactic.MinImports

URI: https://scilib.ai/kg/mathlib#Mathlib.Command.MinImports.getAttrNames

Lean4

/-- `getAttrNames stx` extracts `attribute`s from `stx`.
It does not collect `simp`, `ext`, `to_additive`.
It should collect almost all other attributes, e.g., `fun_prop`. -/
def getAttrNames (stx : Syntax) : NameSet :=
  match stx.find? (·.isOfKind ``Lean.Parser.Term.attributes) with
  | none => { }
  | some stx => getIds stx

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

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

Разделы

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

Аффилиация

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