Documentation

Lean.Util.SCC

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 :
structure Lean.SCC.State (α : Type) [BEq α] [Hashable α] :
@[reducible, inline]
abbrev Lean.SCC.M (α : Type) [BEq α✝] [Hashable α✝] (α : Type) :
Equations
def Lean.SCC.scc {α : Type} [BEq α] [Hashable α] (vertices : List α) (successorsOf : αList α) :
List (List α)
Equations
  • One or more equations did not get rendered due to their size.