splitLengths

Mathlib.Data.List.SplitLengths

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

← MathLib Explorer

English

The length of the list sz.splitLengths l is exactly the length of sz.

Русский

Длина sz.splitLengths l равна длине sz.

LaTeX

$$$ (sz.splitLengths\\ l).length = sz.length $$$

Lean4

/-- Split a list to chunks of given lengths.
-/
def splitLengths : List ℕ → List α → List (List α)
  | [], _ => []
  | n :: ns, x =>
    let (x0, x1) := x.splitAt n
    x0 :: ns.splitLengths x1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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