rtake

Mathlib.Data.List.DropRight

URI: https://scilib.ai/kg/mathlib#List.rtake

English

Take the last n elements of a list: rtake l n = drop (length l − n) l.

Русский

Возьмем последние n элемента списка: rtake l n = drop (длина(l) − n) l.

LaTeX

$$$\\text{rtake} = \\text{drop}_{l.length - n}$$$

Lean4

/-- Take `n` elements from the tail end of a list. -/
def rtake : List α :=
  l.drop (l.length - n)

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

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

Разделы

Аффилиация

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