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

@[deprecated Array.forIn_eq_forIn_toList (since := "2024-09-09")]

theorem Array.forIn_eq_forIn_data {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

Alias of Array.forIn_eq_forIn_toList.

@[deprecated Array.forIn_eq_forIn_data (since := "2024-08-13")]

theorem Array.forIn_eq_data_forIn {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

Alias of Array.forIn_eq_forIn_toList.

---

Alias of Array.forIn_eq_forIn_toList.

zipWith / zip

@[deprecated Array.toList_zipWith (since := "2024-09-09")]

theorem Array.data_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) : (zipWith f as bs).toList = List.zipWith f as.toList bs.toList

Alias of Array.toList_zipWith.

@[deprecated Array.data_zipWith (since := "2024-08-13")]

theorem Array.zipWith_eq_zipWith_data {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) : (zipWith f as bs).toList = List.zipWith f as.toList bs.toList

Alias of Array.toList_zipWith.

---

Alias of Array.toList_zipWith.

flatten

@[deprecated Array.toList_flatten (since := "2024-09-09")]

theorem Array.data_join {α : Type u_1} {l : Array (Array α)} : l.flatten.toList = (List.map toList l.toList).flatten

Alias of Array.toList_flatten.

@[deprecated Array.toList_flatten (since := "2024-08-13")]

theorem Array.join_data {α : Type u_1} {l : Array (Array α)} : l.flatten.toList = (List.map toList l.toList).flatten

Alias of Array.toList_flatten.

@[deprecated Array.mem_flatten (since := "2024-10-15")]

theorem Array.mem_join {α : Type u_1} {a : α} {L : Array (Array α)} : a ∈ L.flatten ↔ ∃ (l : Array α), l ∈ L ∧ a ∈ l

Alias of Array.mem_flatten.

indexOf?

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

erase

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

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-03")]

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

@[simp]

theorem Array.size_insertIdx {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) : (as.insertIdx i v h).size = as.size + 1

@[deprecated Array.size_insertIdx (since := "2024-11-20")]

theorem Array.size_insertAt {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) : (as.insertIdx i v h).size = as.size + 1

Alias of Array.size_insertIdx.

@[irreducible]

theorem Array.getElem_insertIdx_loop_lt {α : Type u_1} {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h : k < (insertIdx.loop i as j).size} (w : k < i) : (insertIdx.loop i as j)[k] = as[k]

@[irreducible]

theorem Array.getElem_insertIdx_loop_eq {α : Type u_1} {as : Array α} {i j : Nat} {hj : j < as.size} {h : i < (insertIdx.loop i as ⟨j, hj⟩).size} : (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]

@[irreducible]

theorem Array.getElem_insertIdx_loop_gt {α : Type u_1} {as : Array α} {i j : Nat} {hj : j < as.size} {k : Nat} {h : k < (insertIdx.loop i as ⟨j, hj⟩).size} (w : i < k) : (insertIdx.loop i as ⟨j, hj⟩)[k] = if k ≤ j then as[k - 1] else as[k]

theorem Array.getElem_insertIdx_loop {α : Type u_1} {as : Array α} {i j : Nat} {hj : j < as.size} {k : Nat} {h : k < (insertIdx.loop i as ⟨j, hj⟩).size} : (insertIdx.loop i as ⟨j, hj⟩)[k] = if h₁ : k < i then as[k] else if h₂ : k = i then if i ≤ j then as[j] else as[i] else if k ≤ j then as[k - 1] else as[k]

theorem Array.getElem_insertIdx {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) (k : Nat) (h' : k < (as.insertIdx i v h).size) : (as.insertIdx i v h)[k] = if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

theorem Array.getElem_insertIdx_lt {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) (k : Nat) (h' : k < (as.insertIdx i v h).size) (h✝ : k < i) : (as.insertIdx i v h)[k] = as[k]

@[deprecated Array.getElem_insertIdx_lt (since := "2024-11-20")]

theorem Array.getElem_insertAt_lt {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) (k : Nat) (h' : k < (as.insertIdx i v h).size) (h✝ : k < i) : (as.insertIdx i v h)[k] = as[k]

Alias of Array.getElem_insertIdx_lt.

theorem Array.getElem_insertIdx_eq {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) : (as.insertIdx i v h)[i] = v

@[deprecated Array.getElem_insertIdx_eq (since := "2024-11-20")]

theorem Array.getElem_insertAt_eq {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) : (as.insertIdx i v h)[i] = v

Alias of Array.getElem_insertIdx_eq.

theorem Array.getElem_insertIdx_gt {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) (k : Nat) (h' : k < (as.insertIdx i v h).size) (h✝ : i < k) : (as.insertIdx i v h)[k] = as[k - 1]

@[deprecated Array.getElem_insertIdx_gt (since := "2024-11-20")]

theorem Array.getElem_insertAt_gt {α : Type u_1} (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) (k : Nat) (h' : k < (as.insertIdx i v h).size) (h✝ : i < k) : (as.insertIdx i v h)[k] = as[k - 1]

Alias of Array.getElem_insertIdx_gt.