English
Split a sequence at n into a finite initial segment of length n (as a list) and a remaining tail sequence.
Русский
Разделить последовательность на префикс длины n (как список) и остаток-последовательность.
LaTeX
$$$ splitAt : \mathbb{N} \to \mathrm{Seq}(\alpha) \to \mathrm{List}(\alpha) \times \mathrm{Seq}(\alpha),\quad 0, s \mapsto ([], s),\qquad n+1, s \mapsto \begin{cases} ([],\mathrm{nil}) & \text{if } s \text{ terminates} \\ (x::l, r) & \text{if } s = x::s' \text{ and } (l,r) = splitAt(n, s'). \end{cases}$$$
Lean4
/-- Split a sequence at `n`, producing a finite initial segment
and an infinite tail. -/
def splitAt : ℕ → Seq α → List α × Seq α
| 0, s => ([], s)
| n + 1, s =>
match destruct s with
| none => ([], nil)
| some (x, s') =>
let (l, r) := splitAt n s'
(List.cons x l, r)
