drop

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.drop

English

Drop removes the first n elements: drop(s,0)=s and drop(s,n+1)=tail(drop(s,n)).

Русский

Удаление удаляет первые n элементов: drop(s,0)=s и drop(s,n+1)=tail(drop(s,n)).

LaTeX

$$$$\text{drop}(s,0)=s,\quad \text{drop}(s,n+1)=\text{tail}(\text{drop}(s,n)).$$$$

Lean4

/-- drop the first `n` elements from `s`. -/
def drop (s : WSeq α) : ℕ → WSeq α
  | 0 => s
  | n + 1 => tail (drop s n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru