importPath — Mathlib

Lean4
/-- Find the dependency chain, starting at a module that imports `imported`, and ends with the
current module.

The path only contains the intermediate steps: it excludes `imported` and the current module.
-/
def importPath (env : Environment) (imported : Name) : Array Name :=
  Id.run
    (do
      let mut result := #[]
      let modData := env.header.moduleData
      let modNames := env.header.moduleNames
      if let some idx := env.getModuleIdx? imported then
        let mut target := imported
        for i in [idx.toNat + 1:modData.size]do
          if modData[i]!.imports.any (·.module == target) then
            target := modNames[i]!
            result := result.push modNames[i]!
      return result)
Похожие утверждения