def Hex.GraphIso.Label.toArray {n : Nat} (l : Label n) : Array Nat

The raw position-to-vertex array of a typed canonical labelling.

Equations

• l.toArray = Array.ofFn fun (i : Fin n) => ↑(l.get i)

@[simp]

theorem Hex.GraphIso.Label.size_toArray {n : Nat} (l : Label n) : l.toArray.size = n

theorem Hex.GraphIso.Label.ofArray?_toArray {n : Nat} {lab : Array Nat} {l : Label n} (h : ofArray? n lab = some l) : l.toArray = lab

Parsing preserves the entire raw array.

theorem Hex.GraphIso.Label.ofArray?_exists {n : Nat} {lab : Array Nat} (hperm : lab.toList.Perm (List.range n)) : ∃ (l : Label n), ofArray? n lab = some l

Every permutation array passes the executed public label parser.