@[inline]

def Hex.SparseGraph.packStep {α : Type u_1} (acc : Array Nat × Array α) (row : List α) : Array Nat × Array α

Equations

• Hex.SparseGraph.packStep (offsets, neighbors) row = (offsets.push neighbors.size, neighbors ++ row)

def Hex.SparseGraph.pack {α : Type u_1} (rows : List (List α)) : Array Nat × Array α

Append each row directly to its final array, recording offsets in the same pass. No flattened intermediate list or row-length scan is needed.

Equations

• Hex.SparseGraph.pack rows = match List.foldl Hex.SparseGraph.packStep (#[], #[]) rows with | (offsets, neighbors) => (offsets.push neighbors.size, neighbors)

theorem Hex.SparseGraph.pack_eq {α : Type u_1} (rows : List (List α)) : pack rows = ((offsetsOf rows).toArray, rows.flatten.toArray)

def Hex.SparseGraph.ofRowsFast {n : Nat} (rows : Vector (List (Fin n)) n) (hs : ∀ (i : Fin n), List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) rows[i]) (hr : ∀ (i j : Fin n), j ∈ rows[i] ↔ i ∈ rows[j]) (hl : ∀ (i : Fin n), ¬i ∈ rows[i]) : SparseGraph n

The checked graph constructor with direct array packing.

Equations

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

@[csimp]

theorem Hex.SparseGraph.ofRows_eq_fast : @ofRows = @ofRowsFast