Documentation

ImportGraph.Imports.ImportGraph

source
def Lean.Environment.importsOf (env : Environment) (n : Name) :
Array Name

Find the imports of a given module.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Environment.importGraph (env : Environment) :
    NameMap (Array Name)

    Construct the import graph of the current file.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For