def Hex.GraphIso.Nauty.Sparse.Literal.bestcell {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level : Nat) : Nat

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.targetcell {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) : Nat

Honour a valid hint, otherwise use sparse best-cell selection through the target level and the first nontrivial cell at greater depths.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Literal.maketargetcell {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) : Nat × VSet n × Nat

Equations

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

@[specialize #[]]

def Hex.GraphIso.Nauty.Sparse.Literal.initialPartitionWith {α : Type u_1} (n k : Nat) (colors : Array α) (color : α → Nat) : Array Nat × List Nat

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.bestcell_eq : @bestcell = @Sparse.bestcell

theorem Hex.GraphIso.Nauty.Sparse.Literal.targetcell_eq : @targetcell = @Sparse.targetcell

theorem Hex.GraphIso.Nauty.Sparse.Literal.maketargetcell_eq : @maketargetcell = @Sparse.maketargetcell

theorem Hex.GraphIso.Nauty.Sparse.Literal.initialPartitionWith_eq : @initialPartitionWith = @Sparse.initialPartitionWith