Definitions for List not (yet) in Std

ink

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

• List.nthLe l n h = List.get l { val := n, isLt := h }

ink

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 }

ink

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

• List.headI x = match x with | [] => default | a :: tail => a

ink

@[simp]

theorem List.headI_nil {α : Type u_1} [inst : Inhabited α] : List.headI [] = default

ink

@[simp]

theorem List.headI_cons {α : Type u_1} [inst : Inhabited α] {h : α} {t : List α} : List.headI (h :: t) = h

ink

def List.findIndex {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] : List α → ℕ

Find index of element with given property.

Equations

• List.findIndex p = List.findIdx fun b => decide (p b)

ink

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

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

Equations

• List.getLastI [] = default
• List.getLastI [a] = a
• List.getLastI [head, b] = b
• List.getLastI (head :: head_1 :: l) = List.getLastI l

ink

@[inline]

def List.ret {α : Type u} (a : α) : List α

List with a single given element.

Equations

• List.ret a = [a]

ink

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

≤≤ implies not > for lists.