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 :
Instances For
    structure Lean.SCC.State (α : Type) [BEq α] [Hashable α] :
    Instances For
      @[inline, reducible]
      abbrev Lean.SCC.M (α : Type) [BEq α✝] [Hashable α✝] (α : Type) :
      Equations
      Instances For
        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.
        Instances For