toArray #
next? #
dropLast #
set #
tail #
eraseP #
erase #
findIdx? #
replaceF #
@[simp]
disjoint #
@[simp]
@[simp]
union #
inter #
product #
monadic operations #
theorem
List.forIn_eq_bindList
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → β → m (ForInStep β))
(l : List α)
(init : β)
:
diff #
drop #
Chain #
range', range #
@[deprecated List.getElem?_range (since := "2024-06-12")]
indexOf and indexesOf #
@[simp]
@[deprecated List.eraseIdx_idxOf_eq_erase (since := "2025-01-30")]
Alias of List.eraseIdx_idxOf_eq_erase
.
@[deprecated List.idxOf_mem_indexesOf (since := "2025-01-30")]
theorem
List.indexOf_mem_indexesOf
{α : Type u_1}
{x : α}
[BEq α]
[LawfulBEq α]
{xs : List α}
(m : x ∈ xs)
:
Alias of List.idxOf_mem_indexesOf
.
insertP #
dropPrefix?, dropSuffix?, dropInfix? #
@[simp]
@[simp]
@[irreducible]
deprecations #
@[deprecated List.modify_nil (since := "2024-10-21")]
Alias of List.modify_nil
.
@[deprecated List.modify_zero_cons (since := "2024-10-21")]
Alias of List.modify_zero_cons
.
@[deprecated List.modifyTailIdx_id (since := "2024-10-21")]
Alias of List.modifyTailIdx_id
.
@[deprecated List.eraseIdx_eq_modifyTailIdx (since := "2024-10-21")]
Alias of List.eraseIdx_eq_modifyTailIdx
.
@[deprecated List.length_modifyTailIdx (since := "2024-10-21")]
theorem
List.length_modifyNthTail
{α : Type u_1}
(f : List α → List α)
(H : ∀ (l : List α), (f l).length = l.length)
(n : Nat)
(l : List α)
:
Alias of List.length_modifyTailIdx
.
@[deprecated List.length_modifyTailIdx (since := "2024-06-07")]
theorem
List.modifyNthTail_length
{α : Type u_1}
(f : List α → List α)
(H : ∀ (l : List α), (f l).length = l.length)
(n : Nat)
(l : List α)
:
Alias of List.length_modifyTailIdx
.
@[deprecated List.modifyTailIdx_add (since := "2024-10-21")]
Alias of List.modifyTailIdx_add
.
@[deprecated List.exists_of_modifyTailIdx (since := "2024-10-21")]
theorem
List.exists_of_modifyNthTail
{α : Type u_1}
(f : List α → List α)
{n : Nat}
{l : List α}
(h : n ≤ l.length)
:
Alias of List.exists_of_modifyTailIdx
.
@[deprecated List.length_modify (since := "2024-10-21")]
Alias of List.length_modify
.
@[deprecated List.length_modify (since := "2024-06-07")]
Alias of List.length_modify
.
@[deprecated List.exists_of_modify (since := "2024-10-21")]
theorem
List.exists_of_modifyNth
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < l.length)
:
Alias of List.exists_of_modify
.
@[deprecated List.modify_eq_take_drop (since := "2024-10-21")]
Alias of List.modify_eq_take_drop
.
@[deprecated List.set_eq_modify (since := "2024-10-21")]
Alias of List.set_eq_modify
.
@[deprecated List.modify_eq_set_get? (since := "2024-10-21")]
Alias of List.modify_eq_set_get?
.
@[deprecated List.modify_eq_set_get (since := "2024-10-21")]
theorem
List.modifyNth_eq_set_get
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < l.length)
:
Alias of List.modify_eq_set_get
.
@[deprecated List.getElem?_set_self' (since := "2024-06-12")]