getVisited

Mathlib.Tactic.MinImports

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

Lean4

/-- Extracts the names of the declarations in `env` on which `decl` depends. -/
def getVisited (decl : Name) : CommandElabM NameSet := do
  unless (← hasConst decl) do
    return
      { }
        -- without resetting the state, the "unused tactics" linter gets confused?

  let st ← get
  liftCoreM decl.transitivelyUsedConstants <* set st

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

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

Разделы

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

Аффилиация

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