def Hex.SparseGraph.Builder.mapRow {n : Nat} (xs : Array (Fin n)) (f : Fin n → Fin n) : List (Fin n)

Map and normalize a compressed row.

Equations

• Hex.SparseGraph.Builder.mapRow xs f = Hex.SparseGraph.Builder.normalize (List.map f xs.toList)

@[specialize #[]]

def Hex.SparseGraph.Builder.countRow {n : Nat} (xs : Array (Fin n)) (f : Fin n → Fin n) : List (Fin n)

Emit a row in vertex order using a temporary membership array.

Equations

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

theorem Hex.SparseGraph.Builder.countRow_eq {n : Nat} (xs : Array (Fin n)) (f : Fin n → Fin n) : countRow xs f = mapRow xs f

@[inline]

def Hex.SparseGraph.Builder.mapRowFast {n : Nat} (xs : Array (Fin n)) (f : Fin n → Fin n) : List (Fin n)

Use counting only when its vertex scan is bounded by eight times the row length. Sparse rows keep the existing merge sort.

Equations

• Hex.SparseGraph.Builder.mapRowFast xs f = if n ≤ 8 * xs.size then Hex.SparseGraph.Builder.countRow xs f else Hex.SparseGraph.Builder.normalize (List.map f xs.toList)

@[csimp]

theorem Hex.SparseGraph.Builder.mapRow_eq_fast : @mapRow = @mapRowFast