def Hex.GraphIso.Nauty.Sparse.Sort.median (a b c : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.Sparse.Sort.median a b c = if a ≤ b then if b ≤ c then b else if c ≤ a then a else c else if a ≤ c then a else if c ≤ b then b else c

def Hex.GraphIso.Nauty.Sparse.Sort.insertion (x y : Array Nat) (start len : Nat) : Array Nat

Insertion sort for the short segments in sortindirect. Equal keys stay in their current order in this branch.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Sort.pivot (x y : Array Nat) (start len : Nat) : Nat

Pinned pivot sampling, including the median-of-nine threshold.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Sort.partition (x y : Array Nat) (start len : Nat) : Array Nat × Nat × Nat

Bentley–McIlroy partition with nauty's exact swaps. Right cursors are exclusive, avoiding C's temporary pointer just before the array.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Sort.indirect (x y : Array Nat) (start len : Nat) : Array Nat

The exact indirect sort used for three or more count fragments. The explicit stack preserves nauty's smaller-side-first traversal. Each partition removes its nonempty pivot class, so fewer than 2 * len stack entries are processed.

Equations

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