recNeNil

Mathlib.Data.List.Induction

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

Lean4

/-- A dependent recursion principle for nonempty lists. Useful for dealing with
operations like `List.head` which are not defined on the empty list.
-/
@[elab_as_elim]
def recNeNil {motive : (l : List α) → l ≠ [] → Sort*} (singleton : ∀ x, motive [x] (cons_ne_nil x []))
    (cons : ∀ x xs h, motive xs h → motive (x :: xs) (cons_ne_nil x xs)) (l : List α) (h : l ≠ []) : motive l h :=
  match l with
  | [x] => singleton x
  | x :: y :: xs => cons x (y :: xs) (cons_ne_nil y xs) (recNeNil singleton cons (y :: xs) (cons_ne_nil y xs))

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

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

Разделы

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

Аффилиация

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