findImports

Mathlib.Tactic.Linter.DirectoryDependency

URI: https://scilib.ai/kg/mathlib#findImports

Lean4

/-- Parse all imports in a text file at `path` and return just their names:
this is just a thin wrapper around `Lean.parseImports'`.
Omit `Init` (which is part of the prelude). -/
def findImports (path : System.FilePath) : IO (Array Lean.Name) := do
  return
    (← Lean.parseImports' (← IO.FS.readFile path) path.toString).imports |>.map (fun imp ↦ imp.module) |>.erase `Init

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

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

Разделы

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

Аффилиация

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