importsBelow

Mathlib.Tactic.Linter.MinImports

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

Lean4

/-- `importsBelow tc ms` takes as input a `NameMap NameSet` `tc`, representing the
`transitiveClosure` of the imports of the current module, and a `NameSet` of module names `ms`.
It returns the modules that are transitively imported by `ms`, using the data in `tc`.
-/
def importsBelow (tc : NameMap NameSet) (ms : NameSet) : NameSet :=
  ms.foldl (·.append <| tc.getD · default) ms

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

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

Разделы

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

Аффилиация

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