Transitive closure of a graph

A "graph" in this context is a NameMap (Array Name).

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