English
The length function length(s) returns a Computation ℕ representing the finite length of s (when s is finite).
Русский
Функция длины length(s) возвращает вычисление ℕ, представляющее конечную длину s (если s конечна).
LaTeX
$$$$ \\mathrm{length}: \\mathrm{WSeq}\\ \\alpha \\to \\mathrm{Computation}\\ \\mathbb{N} \\quad \\text{and when } s \\text{ is finite } \\mathrm{length}(s) = |s|. $$$$
Lean4
/-- Get the length of `s` (if it is finite and completes in finite time). -/
def length (s : WSeq α) : Computation ℕ :=
@Computation.corec ℕ (ℕ × WSeq α)
(fun ⟨n, s⟩ =>
match Seq.destruct s with
| none => Sum.inl n
| some (none, s') => Sum.inr (n, s')
| some (some _, s') => Sum.inr (n + 1, s'))
(0, s)
