structure Hex.GraphIso.Nauty.Sparse.Scratch.Marks (n stamp : Nat) (a : Array Nat) : Prop

Allocated generation marks never exceed the current generation.

• size : a.size = n
• bound (i : Nat) : i < n → a[i]! ≤ stamp

theorem Hex.GraphIso.Nauty.Sparse.Scratch.Marks.raise {n stamp next : Nat} {a : Array Nat} (h : Marks n stamp a) (hs : stamp ≤ next) : Marks n next a

theorem Hex.GraphIso.Nauty.Sparse.Scratch.Marks.set {n stamp : Nat} {a : Array Nat} (h : Marks n stamp a) (i : Nat) : Marks n stamp (a.setIfInBounds i stamp)

theorem Hex.GraphIso.Nauty.Sparse.Scratch.Marks.fresh {n stamp i : Nat} {a : Array Nat} (h : Marks n stamp a) (hi : i < n) : a[i]! ≠ stamp + 1

Advancing the generation makes every retained mark stale.