Documentation

Lean.Util.SCC

structure Lean.SCC.Data:

Type

index? : Option Nat
lowlink? : Option Nat
onStack : Bool

structure Lean.SCC.State (α : Type) [inst : BEq α] [inst : Hashable α] :

Type

stack : List α
nextIndex : Nat
data : Std.HashMap α Lean.SCC.Data
sccs : List (List α)

@[inline]

abbrev Lean.SCC.M (α : Type) [inst : BEq α] [inst : Hashable α] (α : Type) :

Type

Equations

Lean.SCC.M α = StateM (Lean.SCC.State α)

def Lean.SCC.scc {α : Type} [inst : BEq α] [inst : Hashable α] (vertices : List α) (successorsOf : α → List α) :

Equations

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