isInMathlib

Mathlib.Tactic.Linter.Header

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.isInMathlib

Lean4

/-- `isInMathlib modName` returns `true` if `Mathlib.lean` imports the file `modName` and `false`
otherwise.
This is used by the `Header` linter as a heuristic of whether it should inspect the file or not.
-/
def isInMathlib (modName : Name) : IO Bool := do
  let mlPath := ("Mathlib" : System.FilePath).addExtension "lean"
  if ← mlPath.pathExists then
    let res ← parseImports' (← IO.FS.readFile mlPath) ""
    return (res.imports.map (·.module == modName)).any (·)
  else
    return false

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

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

Разделы

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

Аффилиация

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