English
Destruct of a mapped sequence equals the computation map of the destruct of the original sequence.
Русский
Разложение отображённой последовательности равно отображению разложения исходной последовательности.
LaTeX
$$$$ \\operatorname{destruct}(\\operatorname{map} f s) = \\operatorname{Computation}.map (\\operatorname{Option.map} (\\operatorname{Prod.map} f (\\operatorname{map} f))) (\\operatorname{destruct} s) $$$$
Lean4
/-- Remove the `n`th element of `s`. -/
def removeNth (s : WSeq α) (n : ℕ) : WSeq α :=
@Seq.corec (Option α) (ℕ × WSeq α)
(fun ⟨n, s⟩ =>
match Seq.destruct s, n with
| none, _ => none
| some (none, s'), n => some (none, n, s')
| some (some a', s'), 0 => some (some a', 0, s')
| some (some _, s'), 1 => some (none, 0, s')
| some (some a', s'), n + 2 => some (some a', n + 1, s'))
(n + 1, s)
