Definitions for List not (yet) in Batteries

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[inline, deprecated List.pure]

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

List with a single given element.

Equations

• List.ret a = [a]

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

≤ implies not > for lists.