theorem Hex.GraphIso.Nauty.Sparse.compact_scan (before : Array Nat) (p : Nat → Bool) (first last : Nat) (hf : first ≤ last) (hb : last ≤ before.size) : have t := (have lab := before; have v2 := first; have hit := #[]; do let __s ← forIn [first:last] (lab, v2, hit) fun (j : Nat) (__s : Array Nat × Nat × Array Nat) => have lab := __s.fst; have __s := __s.snd; have v2 := __s.fst; have hit := __s.snd; have v := lab[j]!; if p v = true then have hit := hit.push v; pure (ForInStep.yield (lab, v2, hit)) else have lab := lab.set! v2 v; have v2 := v2 + 1; pure (ForInStep.yield (lab, v2, hit)) have lab : Array Nat := __s.fst have __s : Nat × Array Nat := __s.snd have v2 : Nat := __s.fst have hit : Array Nat := __s.snd pure (lab, v2, hit)).run; Compact before p first last (List.map (fun (q : Nat) => before[q]!) (List.range' first (last - first))) t.fst t.snd.snd t.snd.fst

The singleton splitter's actual compaction loop retains unmarked vertices in order and collects marked vertices in order, even when writes alias the position currently being read.