def Hex.GraphIso.Nauty.Sparse.sortCells (xs : Array Nat) : Array Nat

Numeric ordering of distinct touched-cell starts.

Equations

• Hex.GraphIso.Nauty.Sparse.sortCells xs = (Hex.List.sort xs.toList fun (x1 x2 : Nat) => decide (x1 ≤ x2)).toArray

@[inline]

def Hex.GraphIso.Nauty.Sparse.sortCellsFast (xs : Array Nat) : Array Nat

Tiny touched sets need only direct comparisons; larger sets retain the existing verified merge sort.

Equations

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

@[csimp]

theorem Hex.GraphIso.Nauty.Sparse.sortCells_eq_fast : sortCells = sortCellsFast