- stack : List α
- nextIndex : Nat
- data : Std.HashMap α Lean.SCC.Data
- sccs : List (List α)
@[inline]
Equations
- Lean.SCC.M α = StateM (Lean.SCC.State α)
def
Lean.SCC.scc
{α : Type}
[inst : BEq α]
[inst : Hashable α]
(vertices : List α)
(successorsOf : α → List α)
:
Equations
- Lean.SCC.scc vertices successorsOf = let main := List.forM vertices fun a => do let aData ← Lean.SCC.getDataOf a if Option.isNone aData.index? = true then Lean.SCC.sccAux successorsOf a else pure PUnit.unit; let x := StateT.run main { stack := [], nextIndex := 0, data := ∅, sccs := [] }; match x with | (x, s) => List.reverse s.sccs