def Hex.GraphIso.Nauty.Sparse.runColored {n k : Nat} (G : Sparse.Colored n k) : State n

Run the sparse search from a native coloured graph.

Equations

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

def Hex.GraphIso.Nauty.Sparse.searchResult? {n k : Nat} (G : Sparse.Colored n k) : Option (Sparse.CanonResult n k)

Diagnostic checked canonical graph and label. Sparse.Result proves unconditional success; the total API extracts this same result.

Equations

• Hex.GraphIso.Nauty.Sparse.searchResult? G = do let l ← Hex.GraphIso.Label.ofArray? n (Hex.GraphIso.Nauty.Sparse.runColored G).canonlab pure { form := G.relabel l, label := l }

theorem Hex.GraphIso.Nauty.Sparse.searchResult?_relabel {n k : Nat} {G : Sparse.Colored n k} {r : Sparse.CanonResult n k} (h : searchResult? G = some r) : r.form = G.relabel r.label