Documentation

Mathlib.Init.Data.List.Basic

Definitions for List not (yet) in Std

def List.nthLe {α : Type u_1} (l : List α) (n : ) (h : n < List.length l) :
α

nth element of a list l given n < l.length.

Equations
theorem List.nthLe_eq {α : Type u_1} (l : List α) (n : ) (h : n < List.length l) :
List.nthLe l n h = List.get l { val := n, isLt := h }
def List.headI {α : Type u_1} [inst : Inhabited α] :
List αα

The head of a list, or the default element of the type is the list is nil.

Equations
@[simp]
theorem List.headI_nil {α : Type u_1} [inst : Inhabited α] :
List.headI [] = default
@[simp]
theorem List.headI_cons {α : Type u_1} [inst : Inhabited α] {h : α} {t : List α} :
List.headI (h :: t) = h
def List.findIndex {α : Type u_1} (p : αProp) [inst : DecidablePred p] :
List α

Find index of element with given property.

Equations
def List.getLastI {α : Type u_1} [inst : Inhabited α] :
List αα

The last element of a list, with the default if list empty

Equations
@[inline]
def List.ret {α : Type u} (a : α) :
List α

List with a single given element.

Equations
theorem List.le_eq_not_gt {α : Type u_1} [inst : LT α] (l₁ : List α) (l₂ : List α) :
(l₁ l₂) = ¬l₂ < l₁

≤≤ implies not > for lists.