Very simple implementation of Tarjan's SCC algorithm. Performance is not a goal here since we use this module to compiler mutually recursive definitions, where each function (and nested let-rec) in the mutual block is a vertex. So, the graphs are small.

structure Lean.SCC.Data :
Instances For
    structure Lean.SCC.State (α : Type) [inst : BEq α] [inst : Hashable α] :
    Instances For
      abbrev Lean.SCC.M (α : Type) [inst : BEq α] [inst : Hashable α] (α : Type) :
      def Lean.SCC.scc {α : Type} [inst : BEq α] [inst : Hashable α] (vertices : List α) (successorsOf : αList α) :
      List (List α)
      • One or more equations did not get rendered due to their size.