swapFirstTwo

Mathlib.Tactic.ToAdditive.Frontend

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

Lean4

/-- Swap the first two elements of a list -/
def _root_.List.swapFirstTwo {α : Type _} : List α → List α
  | [] => []
  | [x] => [x]
  | x :: y :: l => y :: x :: l

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

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

Разделы

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

Аффилиация

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