take — Mathlib

English

take n s returns the first n elements of s as a list.

Русский

take n s возвращает первые n элементов потока s в виде списка.

LaTeX

$$$ \text{take}(0,s) = [],\quad \text{take}(n+1,s) = \text{List.cons}(\text{head}(s),\ \text{take}(n,\text{tail}(s))). $$$

Lean4

/-- `take n s` returns a list of the `n` first elements of stream `s` -/
def take : ℕ → Stream' α → List α
  | 0, _ => []
  | n + 1, s => List.cons (head s) (take n (tail s))

Похожие утверждения