HepLean Documentation

Mathlib.Data.List.GetD

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.

source
theorem List.getD_eq_getElem {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : n < l.length) :
l.getD n d = l[n]
source
@[deprecated List.getD_eq_getElem]
theorem List.getD_eq_get {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : n < l.length) :
l.getD n d = l.get ⟨n, hn⟩
source
theorem List.getD_map {α : Type u} {β : Type v} (l : List α) (d : α) {n : ℕ} (f : α → β) :
(List.map f l).getD n (f d) = f (l.getD n d)
source
theorem List.getD_eq_default {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : l.length ≤ n) :
l.getD n d = d
source
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 α.

Equations
Instances For
    source
    @[simp]
    theorem List.getElem?_getD_singleton_default_eq {α : Type u} (d : α) (n : ℕ) :
    [d][n]?.getD d = d
    source
    @[deprecated List.getElem?_getD_singleton_default_eq]
    theorem List.getD_singleton_default_eq {α : Type u} (d : α) (n : ℕ) :
    [d][n]?.getD d = d

    Alias of List.getElem?_getD_singleton_default_eq.

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

    Alias of List.getElem?_getD_replicate_default_eq.

    source
    theorem List.getD_append {α : Type u} (l l' : List α) (d : α) (n : ℕ) (h : n < l.length) :
    (l ++ l').getD n d = l.getD n d
    source
    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
    source
    theorem List.getD_eq_getD_get? {α : Type u} (l : List α) (d : α) (n : ℕ) :
    l.getD n d = (l.get? n).getD d
    source
    @[simp]
    theorem List.getI_nil {α : Type u} (n : ℕ) [Inhabited α] :
    [].getI n = default
    source
    @[simp]
    theorem List.getI_cons_zero {α : Type u} (x : α) (xs : List α) [Inhabited α] :
    (x :: xs).getI 0 = x
    source
    @[simp]
    theorem List.getI_cons_succ {α : Type u} (x : α) (xs : List α) (n : ℕ) [Inhabited α] :
    (x :: xs).getI (n + 1) = xs.getI n
    source
    theorem List.getI_eq_getElem {α : Type u} (l : List α) [Inhabited α] {n : ℕ} (hn : n < l.length) :
    l.getI n = l[n]
    source
    @[deprecated List.getI_eq_getElem]
    theorem List.getI_eq_get {α : Type u} (l : List α) [Inhabited α] {n : ℕ} (hn : n < l.length) :
    l.getI n = l.get ⟨n, hn⟩
    source
    theorem List.getI_eq_default {α : Type u} (l : List α) [Inhabited α] {n : ℕ} (hn : l.length ≤ n) :
    l.getI n = default
    source
    theorem List.getD_default_eq_getI {α : Type u} (l : List α) [Inhabited α] {n : ℕ} :
    l.getD n default = l.getI n
    source
    theorem List.getI_append {α : Type u} [Inhabited α] (l l' : List α) (n : ℕ) (h : n < l.length) :
    (l ++ l').getI n = l.getI n
    source
    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)
    source
    theorem List.getI_eq_iget_get? {α : Type u} (l : List α) [Inhabited α] (n : ℕ) :
    l.getI n = (l.get? n).iget
    source
    theorem List.getI_eq_iget_getElem? {α : Type u} (l : List α) [Inhabited α] (n : ℕ) :
    l.getI n = l[n]?.iget
    source
    theorem List.getI_zero_eq_headI {α : Type u} (l : List α) [Inhabited α] :
    l.getI 0 = l.headI