splitEvenOdd

Mathlib.Tactic.CategoryTheory.Coherence.Basic

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.BicategoryLike.List.splitEvenOdd

Lean4

/-- List.splitEvenOdd [0, 1, 2, 3, 4] = ([0, 2, 4], [1, 3]) -/
def splitEvenOdd {α : Type u} : List α → List α × List α
  | [] => ([], [])
  | [a] => ([a], [])
  | a :: b :: xs =>
    let (as, bs) := List.splitEvenOdd xs
    (a :: as, b :: bs)

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

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

Разделы

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

Аффилиация

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