English
Take the first n elements of a sequence, producing a finite list.
Русский
Взять первые n элементов последовательности, получив конечный список.
LaTeX
$$$ \mathrm{take} : \mathbb{N} \to \mathrm{Seq}(\alpha) \to \mathrm{List}(\alpha),\quad \text{take}(0,s) = [],\ \text{take}(n+1,s) = \mathrm{cons}\!\ (\text{x}) \! (\mathrm{take}\, n \; r) \text{ where } s \text{ has head } x \text{ and tail } r.$$$
Lean4
/-- Take the first `n` elements of the sequence (producing a list) -/
def take : ℕ → Seq α → List α
| 0, _ => []
| n + 1, s =>
match destruct s with
| none => []
| some (x, r) => List.cons x (take n r)
