theorem Array.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : forIn as b f = forIn as.toList b f

idxOf?

theorem Array.idxOf?_toList {α : Type u_1} [BEq α] {a : α} {l : Array α} : List.idxOf? a l.toList = l.idxOf? a

finIdxOf?

@[simp]

theorem Array.isSome_finIdxOf?_eq {α : Type u_1} [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} : (xs.finIdxOf? a).isSome = xs.contains a

@[simp]

theorem Array.isNone_finIdxOf?_eq {α : Type u_1} [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} : (xs.finIdxOf? a).isNone = !xs.contains a

erase

@[deprecated List.eraseP_toArray (since := "2025-02-06")]

theorem Array.eraseP_toArray {α : Type u_1} {as : List α} {p : α → Bool} : as.toArray.eraseP p = (List.eraseP p as).toArray

Alias of List.eraseP_toArray.

@[deprecated List.erase_toArray (since := "2025-02-06")]

theorem Array.erase_toArray {α : Type u_1} [BEq α] {as : List α} {a : α} : as.toArray.erase a = (as.erase a).toArray

Alias of List.erase_toArray.

@[simp]

theorem Array.toList_erase {α : Type u_1} [BEq α] (l : Array α) (a : α) : (l.erase a).toList = l.toList.erase a

@[simp]

theorem Array.size_eraseIdxIfInBounds {α : Type u_1} (a : Array α) (i : Nat) : (a.eraseIdxIfInBounds i).size = if i < a.size then a.size - 1 else a.size

set

theorem Array.size_set! {α : Type u_1} (a : Array α) (i : Nat) (v : α) : (a.set! i v).size = a.size

map

mem

insertAt

@[deprecated Array.getElem_insertIdx_of_lt (since := "2025-02-06")]

theorem Array.getElem_insertIdx_lt {α : Type u} {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < i) : (xs.insertIdx i x w)[k] = xs[k]

Alias of Array.getElem_insertIdx_of_lt.

@[deprecated Array.getElem_insertIdx_self (since := "2025-02-06")]

theorem Array.getElem_insertIdx_eq {α : Type u} {xs : Array α} {x : α} {i : Nat} (w : i ≤ xs.size) : (xs.insertIdx i x w)[i] = x

Alias of Array.getElem_insertIdx_self.

@[deprecated Array.getElem_insertIdx_of_gt (since := "2025-02-06")]

theorem Array.getElem_insertIdx_gt {α : Type u} {xs : Array α} {x : α} {i k : Nat} (w : k ≤ xs.size) (h : k > i) : (xs.insertIdx i x ⋯)[k] = xs[k - 1]

Alias of Array.getElem_insertIdx_of_gt.