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.

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.

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.

Equations

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

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

Compute the transitive closure of an import graph.

Equations

• m.transitiveClosure = Std.TreeMap.foldl (fun (r : Lean.NameMap Lean.NameSet) (n : Lean.Name) (i : Array Lean.Name) => Lean.NameMap.transitiveClosure.process✝ m r n i) ∅ m

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

Compute the transitive reduction of an import graph.

Typical usage is transitiveReduction (← importGraph).

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

• Core.withImportModules modules f = do let __do_lift ← Lean.findSysroot Lean.initSearchPath __do_lift Core.withImportModules.unsafe_impl_3✝ modules f

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).

Equations

• redundantImports n? = do let env ← Lean.getEnv have imports : Array Lean.Name := env.importsOf (n?.getD env.header.mainModule) pure (env.findRedundantImports imports)