take — Mathlib

English

Take s n returns the first n elements of s as a weak sequence.

Русский

Take s n возвращает первые n элементов последовательности s в виде слабой последовательности.

LaTeX

$$$$ \\mathrm{take}(s, n) : \\mathrm{WSeq}\\, \\alpha $$$$

Lean4

/-- Get the first `n` elements of a weak sequence -/
def take (s : WSeq α) (n : ℕ) : WSeq α :=
  @Seq.corec (Option α) (ℕ × WSeq α)
    (fun ⟨n, s⟩ =>
      match n, Seq.destruct s with
      | 0, _ => none
      | _ + 1, none => none
      | m + 1, some (none, s') => some (none, m + 1, s')
      | m + 1, some (some a, s') => some (some a, m, s'))
    (n, s)

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