The following functions can't be defined at Init.Data.List.Basic, because they depend on Init.Util, and Init.Util depends on Init.Data.List.Basic.

Alternative getters

get?

@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]

def List.get? {α : Type u_1} (as : List α) (i : Nat) : Option α

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function returns none. Also see get, getD and get!.

Equations

• (a :: tail).get? 0 = some a
• (head :: as).get? n.succ = as.get? n
• x✝¹.get? x✝ = none

@[simp, deprecated "Use `a[i]?` instead." (since := "2025-02-12")]

theorem List.get?_nil {α : Type u_1} {n : Nat} : [].get? n = none

@[simp, deprecated "Use `a[i]?` instead." (since := "2025-02-12")]

theorem List.get?_cons_zero {α : Type u_1} {a : α} {l : List α} : (a :: l).get? 0 = some a

@[simp, deprecated "Use `a[i]?` instead." (since := "2025-02-12")]

theorem List.get?_cons_succ {α : Type u_1} {a : α} {l : List α} {n : Nat} : (a :: l).get? (n + 1) = l.get? n

@[deprecated "Use `List.ext_getElem?`." (since := "2025-02-12")]

theorem List.ext_get? {α : Type u_1} {l₁ l₂ : List α} : (∀ (n : Nat), l₁.get? n = l₂.get? n) → l₁ = l₂

get!

@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]

def List.get! {α : Type u_1} [Inhabited α] (as : List α) (i : Nat) : α

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function panics when executed, and returns default. See get? and getD for safer alternatives.

Equations

• (a :: tail).get! 0 = a
• (head :: as).get! n.succ = as.get! n
• x✝¹.get! x✝ = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.get!" 70 18 "invalid index"

@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]

theorem List.get!_nil {α : Type u_1} [Inhabited α] (n : Nat) : [].get! n = default

@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]

theorem List.get!_cons_succ {α : Type u_1} [Inhabited α] (l : List α) (a : α) (n : Nat) : (a :: l).get! (n + 1) = l.get! n

@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]

theorem List.get!_cons_zero {α : Type u_1} [Inhabited α] (l : List α) (a : α) : (a :: l).get! 0 = a

getD

def List.getD {α : Type u_1} (as : List α) (i : Nat) (fallback : α) : α

Returns the element at the provided index, counting from 0. Returns fallback if the index is out of bounds.

To return an Option depending on whether the index is in bounds, use as[i]?. To panic if the index is out of bounds, use as[i]!.

Examples:

• ["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"
• ["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"
• ["spring", "summer", "fall", "winter"].getD 4 "never" = "never"

Equations

• as.getD i fallback = as[i]?.getD fallback

@[simp]

theorem List.getD_nil {n : Nat} {α✝ : Type u_1} {d : α✝} : [].getD n d = d

getLast!

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

Returns the last element in the list. Panics and returns default if the list is empty.

Safer alternatives include:

• getLast?, which returns an Option,
• getLastD, which takes a fallback value for empty lists, and
• getLast, which requires a proof that the list is non-empty.

Examples:

• ["circle", "rectangle"].getLast! = "rectangle"
• ["circle"].getLast! = "circle"

Equations

• [].getLast! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.getLast!" 118 13 "empty list"
• (a :: as).getLast! = (a :: as).getLast ⋯

Head and tail

head!

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

Returns the first element in the list. If the list is empty, panics and returns default.

Safer alternatives include:

• List.head, which requires a proof that the list is non-empty,
• List.head?, which returns an Option, and
• List.headD, which returns an explicitly-provided fallback value on empty lists.

Equations

• [].head! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.head!" 134 12 "empty list"
• (a :: as).head! = a

tail!

def List.tail! {α : Type u_1} : List α → List α

Drops the first element of a nonempty list, returning the tail. If the list is empty, this function panics when executed and returns the empty list.

Safer alternatives include

• tail, which returns the empty list without panicking,
• tail?, which returns an Option, and
• tailD, which returns a fallback value when passed the empty list.

Examples:

• ["apple", "banana", "grape"].tail! = ["banana", "grape"]
• ["banana", "grape"].tail! = ["grape"]

Equations

• [].tail! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.tail!" 153 13 "empty list"
• (a :: as).tail! = as

@[simp]

theorem List.tail!_cons {α : Type u_1} {a : α} {l : List α} : (a :: l).tail! = l

partitionM

@[inline]

def List.partitionM {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α)

Returns a pair of lists that together contain all the elements of as. The first list contains those elements for which the monadic predicate p returns true, and the second contains those for which p returns false. The list's elements are examined in order, from left to right.

This is a monadic version of List.partition.

Example:

def posOrNeg (x : Int) : Except String Bool :=
  if x > 0 then pure true
  else if x < 0 then pure false
  else throw "Zero is not positive or negative"

#eval [-1, 2, 3].partitionM posOrNeg

Except.ok ([2, 3], [-1])

#eval [0, 2, 3].partitionM posOrNeg

Except.error "Zero is not positive or negative"

Equations

• List.partitionM p l = List.partitionM.go✝ p l #[] #[]

partitionMap

@[inline]

def List.partitionMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β ⊕ γ) (l : List α) : List β × List γ

Applies a function that returns a disjoint union to each element of a list, collecting the Sum.inl and Sum.inr results into separate lists.

Examples:

• [0, 1, 2, 3].partitionMap (fun x => if x % 2 = 0 then .inl x else .inr x) = ([0, 2], [1, 3])
• [0, 1, 2, 3].partitionMap (fun x => if x = 0 then .inl x else .inr x) = ([0], [1, 2, 3])

Equations

• List.partitionMap f l = List.partitionMap.go✝ f l #[] #[]

mapMono

This is a performance optimization for List.mapM that avoids allocating a new list when the result of each f a is a pointer equal value a.

For verification purposes, List.mapMono = List.map.

@[implemented_by _private.Init.Data.List.BasicAux.0.List.mapMonoMImp]

def List.mapMonoM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : List α) (f : α → m α) : m (List α)

Applies a monadic function to each element of a list, returning the list of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new list if the result of each function call is pointer-equal to its argument.

Equations

• [].mapMonoM f = pure []
• (a :: as_1).mapMonoM f = do let __do_lift ← f a let __do_lift_1 ← as_1.mapMonoM f pure (__do_lift :: __do_lift_1)

def List.mapMono {α : Type u_1} (as : List α) (f : α → α) : List α

Applies a function to each element of a list, returning the list of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new list if the result of each function call is pointer-equal to its argument.

For verification purposes, List.mapMono = List.map.

Equations

• as.mapMono f = (as.mapMonoM fun (x : α) => pure (f x)).run

Additional lemmas required for bootstrapping Array.

@[simp]

theorem List.getElem_append_left {α : Type u_1} {i : Nat} {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} : (as ++ bs)[i] = as[i]

@[simp]

theorem List.getElem_append_right {α : Type u_1} {as bs : List α} {i : Nat} (h₁ : as.length ≤ i) {h₂ : i < (as ++ bs).length} : (as ++ bs)[i] = bs[i - as.length]

@[deprecated "Deprecated without replacement." (since := "2025-02-13")]

theorem List.get_last {α : Type u_1} {a : α} {as : List α} {i : Fin (as ++ [a]).length} (h : ¬↑i < as.length) : (as ++ [a]).get i = a

theorem List.sizeOf_lt_of_mem {α : Type u_1} {a : α} [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as

def List.tacticSizeOf_list_dec : Lean.ParserDescr

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf a < sizeOf as when a ∈ as, which is useful for well founded recursions over a nested inductive like inductive T | mk : List T → T.

Equations

• List.tacticSizeOf_list_dec = Lean.ParserDescr.node `List.tacticSizeOf_list_dec 1024 (Lean.ParserDescr.nonReservedSymbol "sizeOf_list_dec" false)

theorem List.append_cancel_left {α : Type u_1} {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs

theorem List.append_cancel_right {α : Type u_1} {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs

@[simp]

theorem List.append_cancel_left_eq {α : Type u_1} (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs)

@[simp]

theorem List.append_cancel_right_eq {α : Type u_1} (as bs cs : List α) : (as ++ bs = cs ++ bs) = (as = cs)

theorem List.sizeOf_get {α : Type u_1} [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as

theorem List.not_lex_antisymm {α : Type u_1} [DecidableEq α] {r : α → α → Prop} [DecidableRel r] (antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y) {as bs : List α} (h₁ : ¬Lex r bs as) (h₂ : ¬Lex r as bs) : as = bs

theorem List.le_antisymm {α : Type u_1} [LT α] [i : Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs

instance List.instAntisymmLeOfNotLt {α : Type u_1} [LT α] [s : Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] : Std.Antisymm fun (x1 x2 : List α) => x1 ≤ x2