English
splitAt s n splits s into a finite initial segment and the tail: splitAt(s,n) yields a computation of (List α × WSeq α) where the list is the reversed initial segment and the tail is the remaining weak sequence.
Русский
splitAt s n разделяет s на конечный начальный фрагмент и хвост: splitAt(s,n) возвращает вычисление (List α × WSeq α), где список — обратимый начальный фрагмент, а хвост — оставшаяся слабая последовательность.
LaTeX
$$$$ \\mathrm{splitAt}(s, n) : \\mathrm{Computation}(\\mathrm{List}\\, \\alpha \\times \\mathrm{WSeq}\\, \\alpha) $$$$
Lean4
/-- Split the sequence at position `n` into a finite initial segment
and the weak sequence tail -/
def splitAt (s : WSeq α) (n : ℕ) : Computation (List α × WSeq α) :=
@Computation.corec (List α × WSeq α) (ℕ × List α × WSeq α)
(fun ⟨n, l, s⟩ =>
match n, Seq.destruct s with
| 0, _ => Sum.inl (l.reverse, s)
| _ + 1, none => Sum.inl (l.reverse, s)
| _ + 1, some (none, s') => Sum.inr (n, l, s')
| m + 1, some (some a, s') => Sum.inr (m, a :: l, s'))
(n, [], s)
