recOnNeNil

Mathlib.Data.List.Induction

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

Lean4

/-- A dependent recursion principle for nonempty lists. Useful for dealing with
operations like `List.head` which are not defined on the empty list.
Same as `List.recNeNil`, with a more convenient argument order.
-/
@[elab_as_elim, simp]
abbrev recOnNeNil {motive : (l : List α) → l ≠ [] → Sort*} (l : List α) (h : l ≠ [])
    (singleton : ∀ x, motive [x] (cons_ne_nil x []))
    (cons : ∀ x xs h, motive xs h → motive (x :: xs) (cons_ne_nil x xs)) : motive l h :=
  recNeNil singleton cons l h

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

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

Разделы

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

Аффилиация

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