List.getD_eq_getD_get?
theorem List.getD_eq_getD_get? : ∀ {α : Type u} (l : List α) (d : α) (n : ℕ), l.getD n d = (l.get? n).getD d
This theorem, `List.getD_eq_getD_get?`, states that for any given type `α`, list `l` of type `α`, default value `d` of type `α`, and natural number `n`, the result of calling the `getD` function on list `l` with index `n` and default value `d` is equal to the result of calling the `getD` function on the result of `get?` function call on the same list `l` with index `n`, using the same default value `d`. Essentially, it asserts that these two ways of retrieving an element from a list at a specific index, providing a default if the index is not valid, are equivalent.
More concisely: For any type `α`, list `l` of length `n+1` over `α`, default value `d` in `α`, and natural number `n`, `getD l n d = getD (get? l n) n d`.
|
List.getD_eq_default
theorem List.getD_eq_default : ∀ {α : Type u} (l : List α) (d : α) {n : ℕ}, l.length ≤ n → l.getD n d = d
This theorem, `List.getD_eq_default`, states that for any type `α`, any list `l` of type `α`, any default value `d` of type `α`, and any natural number `n`, if the length of the list `l` is less than or equal to `n`, then the function `List.getD` applied to the list `l`, the number `n`, and the default value `d` will return the default value `d`. In other words, when trying to access an item at a position in the list that exceeds its length, the function `List.getD` returns the provided default value.
More concisely: For any type `α`, list `l` of length `n` in `α`, and default value `d` in `α`, `List.getD l n d = d` when `n` exceeds the length of `l`.
|
List.getD_eq_get
theorem List.getD_eq_get :
∀ {α : Type u} (l : List α) (d : α) {n : ℕ} (hn : n < l.length), l.getD n d = l.get ⟨n, hn⟩
This theorem, `List.getD_eq_get`, states that for any type `α`, any list `l` of type `α`, any default value `d` of type `α`, and any natural number `n` such that `n` is less than the length of the list `l`, the `getD` function applied to list `l`, index `n`, and default value `d` equals the `get` function applied to the list `l` with a subtype of natural numbers that are less than the length of the list `l`. This asserts that these two ways of accessing an element at a certain index in a list yield the same result when the index is within the bounds of the list.
More concisely: For any type `α`, list `l` of length `n` over `α`, natural number `n`, and default value `d` of type `α`, `getD l n d = get (subtype.range 0 (pred n) l) n d`.
|