How to get the imports for a given module?

Stream: lean4

[Yuri de Wit]

From the Environment, I can get the names of all modules, but how can I get the direct imports for a given module?

[Mario Carneiro]

I don't think this information is stored in the environment. You can call Lean.Elab.parseImports given a lean file to get the list of imports

[Yuri de Wit]

It turns out I had overlooked ModuleData from the EnvironmentHeader:

  for modName in env.allImportedModuleNames do
    let .some modIdx := env.getModuleIdx? modName | panic! s!"Unknown module {modName}"
    let modData := env.header.moduleData.get! modIdx
    for imp in modData.imports do
      dbg_trace s!"{modName} -> {imp}"