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.

@[simp]

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

@[simp]

theorem List.getD_cons_zero {α : Type u} (x : α) (xs : List α) (d : α) : List.getD (x :: xs) 0 d = x

@[simp]

theorem List.getD_cons_succ {α : Type u} (x : α) (xs : List α) (n : ℕ) (d : α) : List.getD (x :: xs) (n + 1) d = List.getD xs n d

theorem List.getD_eq_get {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : n < List.length l) : List.getD l n d = List.get l { val := n, isLt := hn }

@[simp]

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

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

def List.decidableGetDNilNe {α : Type u_1} (a : α) : DecidablePred fun (i : ℕ) => List.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 α.

Equations

• List.decidableGetDNilNe a x = isFalse ⋯

@[simp]

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

@[simp]

theorem List.getD_replicate_default_eq {α : Type u} (d : α) (r : ℕ) (n : ℕ) : List.getD (List.replicate r d) n d = d

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

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

theorem List.getD_eq_getD_get? {α : Type u} (l : List α) (d : α) (n : ℕ) : List.getD l n d = Option.getD (List.get? l n) d

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.getI_eq_get {α : Type u} (l : List α) [Inhabited α] {n : ℕ} (hn : n < List.length l) : List.getI l n = List.get l { val := n, isLt := hn }

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

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

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

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

theorem List.getI_eq_iget_get? {α : Type u} (l : List α) [Inhabited α] (n : ℕ) : List.getI l n = Option.iget (List.get? l n)

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