English
The destruct operation on a weak sequence returns, in computation, either none (empty case) or some (head, tail) when a head exists.
Русский
Операция destruct над слабой последовательностью возвращает в вычислении либо none (пустой случай), либо some (head, tail) когда head существует.
LaTeX
$$$$\text{destruct}: WSeq(\alpha) \to \mathrm{Computation}(\mathrm{Option}(\alpha \times WSeq(\alpha))).$$$$
Lean4
/-- Destruct a weak sequence, to (eventually possibly) produce either
`none` for `nil` or `some (a, s)` if an element is produced. -/
def destruct : WSeq α → Computation (Option (α × WSeq α)) :=
Computation.corec fun s =>
match Seq.destruct s with
| none => Sum.inl none
| some (none, s') => Sum.inr s'
| some (some a, s') => Sum.inl (some (a, s'))
