Definitions for List
not (yet) in Std
nth element of a list l
given n < l.length
.
Equations
- List.nthLe l n h = List.get l { val := n, isLt := h }
theorem
List.nthLe_eq
{α : Type u_1}
(l : List α)
(n : ℕ)
(h : n < List.length l)
:
List.nthLe l n h = List.get l { val := n, isLt := h }
The head of a list, or the default element of the type is the list is nil
.
Equations
- List.headI x = match x with | [] => default | a :: tail => a
@[simp]
@[simp]
theorem
List.headI_cons
{α : Type u_1}
[inst : Inhabited α]
{h : α}
{t : List α}
:
List.headI (h :: t) = h
Find index of element with given property.
Equations
- List.findIndex p = List.findIdx fun b => decide (p b)
The last element of a list, with the default if list empty
Equations
- List.getLastI [] = default
- List.getLastI [a] = a
- List.getLastI [head, b] = b
- List.getLastI (head :: head_1 :: l) = List.getLastI l