def Hex.GraphIso.Nauty.Sparse.Literal.label? (n : Nat) (lab : Array Nat) : Option (Label n)

The checked label parser with exported list-based array mapping.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.label?_eq : label? = Label.ofArray?

def Hex.GraphIso.Nauty.Sparse.Literal.relabel {n : Nat} (G : SparseGraph n) (p : Perm n) : SparseGraph n

Native sparse relabelling with exported function tabulation.

Equations

• Hex.GraphIso.Nauty.Sparse.Literal.relabel G p = Hex.SparseGraph.ofRows (Hex.Vector.ofFn' fun (i : Fin n) => Hex.SparseGraph.Builder.mapRow (G.nbrs (p.get i)) p.inv.get) ⋯ ⋯ ⋯

theorem Hex.GraphIso.Nauty.Sparse.Literal.relabel_eq : @relabel = @SparseGraph.relabel

def Hex.GraphIso.Nauty.Sparse.Literal.leaf {n : Nat} (G : SparseGraph n) (B : Key n) (l : SpecLeaf n) : Option Bool

Compare an actual leaf using native sparse rows and the exported relabelling operations.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.leaf_eq : @leaf = @Replay.leaf