getD and getI

This file provides theorems for working with the getD and getI functions. These are used to access an element of a list by numerical index, with a default value as a fallback when the index is out of range.

theorem List.getD_eq_getElem {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : n < l.length) : l.getD n d = l[n]

theorem List.getD_eq_getElem? {α : Type u} (l : List α) (d : α) (i : Fin l.length) : l.getD (↑i) d = l[i]?.get ⋯

theorem List.getD_eq_get {α : Type u} (l : List α) (d : α) (i : Fin l.length) : l.getD (↑i) d = l.get i

theorem List.getD_map {α : Type u} {β : Type v} (l : List α) (d : α) {n : ℕ} (f : α → β) : (map f l).getD n (f d) = f (l.getD n d)

theorem List.getD_eq_default {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : l.length ≤ n) : l.getD n d = d

theorem List.getD_reverse {α : Type u} {l : List α} (i : ℕ) (h : i < l.length) : l.reverse.getD i = l.getD (l.length - 1 - i)

@[implicit_reducible]

def List.decidableGetDNilNe {α : Type u} (a : α) : DecidablePred fun (i : ℕ) => [].getD i a ≠ a

An empty list can always be decidably checked for the presence of an element. Not an instance because it would clash with DecidableEq α.

@[simp]

theorem List.getElem?_getD_singleton_default_eq {α : Type u} (d : α) (n : ℕ) : [d][n]?.getD d = d

@[simp]

theorem List.getElem?_getD_replicate_default_eq {α : Type u} (d : α) (r n : ℕ) : (replicate r d)[n]?.getD d = d

theorem List.getD_replicate {α : Type u} (x : α) {y : α} {i n : ℕ} (h : i < n) : (replicate n x).getD i y = x

theorem List.getD_append {α : Type u} (l l' : List α) (d : α) (n : ℕ) (h : n < l.length) : (l ++ l').getD n d = l.getD n d

theorem List.getD_append_right {α : Type u} (l l' : List α) (d : α) (n : ℕ) (h : l.length ≤ n) : (l ++ l').getD n d = l'.getD (n - l.length) d

@[deprecated List.getD_eq_getElem?_getD (since := "2025-11-17")]

theorem List.getD_eq_getD_getElem? {α : Type u_1} {l : List α} {i : ℕ} {a : α} : l.getD i a = l[i]?.getD a

Alias of List.getD_eq_getElem?_getD.

theorem List.getD_surjective_iff {α : Type u} {l : List α} {d : α} : (Function.Surjective fun (x : ℕ) => l.getD x d) ↔ ∀ (x : α), x = d ∨ x ∈ l

theorem List.getD_surjective {α : Type u} {l : List α} (h : ∀ (x : α), x ∈ l) (d : α) : Function.Surjective fun (x : ℕ) => l.getD x d

@[simp]

theorem List.getI_nil {α : Type u} (n : ℕ) [Inhabited α] : [].getI n = default

@[simp]

theorem List.getI_cons_zero {α : Type u} (x : α) (xs : List α) [Inhabited α] : (x :: xs).getI 0 = x

@[simp]

theorem List.getI_cons_succ {α : Type u} (x : α) (xs : List α) (n : ℕ) [Inhabited α] : (x :: xs).getI (n + 1) = xs.getI n

theorem List.getI_eq_getElem {α : Type u} (l : List α) [Inhabited α] {n : ℕ} (hn : n < l.length) : l.getI n = l[n]

theorem List.getI_eq_default {α : Type u} (l : List α) [Inhabited α] {n : ℕ} (hn : l.length ≤ n) : l.getI n = default

theorem List.getD_default_eq_getI {α : Type u} (l : List α) [Inhabited α] {n : ℕ} : l.getD n default = l.getI n

theorem List.getI_append {α : Type u} [Inhabited α] (l l' : List α) (n : ℕ) (h : n < l.length) : (l ++ l').getI n = l.getI n

theorem List.getI_append_right {α : Type u} [Inhabited α] (l l' : List α) (n : ℕ) (h : l.length ≤ n) : (l ++ l').getI n = l'.getI (n - l.length)

theorem List.getI_eq_getElem?_getD {α : Type u} (l : List α) [Inhabited α] (n : ℕ) : l.getI n = l[n]?.getD default

@[deprecated List.getI_eq_getElem?_getD (since := "2026-01-05")]

theorem List.getI_eq_iget_getElem? {α : Type u} (l : List α) [Inhabited α] (n : ℕ) : l.getI n = l[n]?.getD default

theorem List.getI_zero_eq_headI {α : Type u} (l : List α) [Inhabited α] : l.getI 0 = l.headI