getAttrs

Mathlib.Tactic.MinImports

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

Lean4

/-- `getAttrs env stx` returns all attribute declaration names contained in `stx` and registered
in the `Environment `env`. -/
def getAttrs (env : Environment) (stx : Syntax) : NameSet :=
  Id.run
    (do
      let mut new : NameSet := { }
      for attr in (getAttrNames stx)do
        match getAttributeImpl env attr with
        | .ok attr =>
          new := new.insert attr.ref
        | .error .. =>
          pure ()
      return new)

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

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

Разделы

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

Аффилиация

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