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

Find the imports of a given module.

def Lean.Environment.importGraph (env : Environment) : NameMap (Array Name)

Construct the import graph of the current file.

def Lean.Environment.findRedundantImports (env : Environment) (imports : Array Name) : NameSet

Return the redundant imports (i.e. those transitively implied by another import) amongst a candidate list of imports.

def Lean.NameMap.transitiveClosure (m : NameMap (Array Name)) : NameMap NameSet

Compute the transitive closure of an import graph.

def Lean.NameMap.transitiveReduction (m : NameMap (Array Name)) : NameMap (Array Name)

Compute the transitive reduction of an import graph.

Typical usage is transitiveReduction (← importGraph).

def Lean.NameMap.downstreamOf (m : NameMap (Array Name)) (targets : NameSet) : NameMap (Array Name)

Restrict an import graph to only the downstream dependencies of some set of modules.

def Lean.NameMap.upstreamOf (m : NameMap (Array Name)) (targets : NameSet) : NameMap (Array Name)

Restrict an import graph to only the transitive imports of some set of modules.

partial def Lean.NameMap.transitiveFilteredUpstream (node : Name) (graph : NameMap (Array Name)) (filter : Name → Bool) (replacement : Option Name := none) : List Name

Filter the list of edges … → node inside graph by the function filter.

Any such upstream node source where filter source returns true will be replaced by all its upstream nodes. This results in a list of all unfiltered nodes in the graph that either had an edge to node or had an indirect edge to node going through filtered nodes.

Will panic if the node is not in the graph.

def Lean.NameMap.filterGraph (graph : NameMap (Array Name)) (filter : Name → Bool) (replacement : Option Name := none) : NameMap (Array Name)

Filters the graph removing all nodes where filter n returns false. Additionally, replace edges from removed nodes by all the transitive edges.

This means there is a path between two nodes in the filtered graph iff there exists such a path in the original graph.

If the optional (replacement : Name) is provided, a corresponding node will be added together with edges to all nodes which had an incoming edge from any filtered node.

def unusedTransitiveImports (amongst : List Lean.Name) (verbose : Bool := false) : Lean.CoreM (List (Lean.Name × List Lean.Name))

Returns a List (Name × List Name) with a key for each module n in amongst, whose corresponding value is the list of modules m in amongst which are transitively imported by n, but no declaration in n makes use of a declaration in m.

def Core.withImportModules (modules : Array Lean.Name) {α : Type} (f : Lean.CoreM α) : IO α

def redundantImports (n? : Option Lean.Name := none) : Lean.CoreM Lean.NameSet

Return the redundant imports (i.e. those transitively implied by another import) of a specified module (or the current module if none is specified).