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.data b f

theorem Array.forIn_eq_forIn_data.loop {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (f : α → β → m (ForInStep β)) {i : Nat} {h : i ≤ as.size} {b : β} {j : Nat} : j + i = as.size → Array.forIn.loop as f i h b = forIn (List.drop j as.data) b f

@[deprecated Array.forIn_eq_forIn_data]

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.data b f

Alias of Array.forIn_eq_forIn_data.

zipWith / zip

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

@[irreducible]

theorem Array.data_zipWith.loop {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : i ≤ as.size → i ≤ bs.size → (Array.zipWithAux f as bs i cs).data = cs.data ++ List.zipWith f (List.drop i as.data) (List.drop i bs.data)

@[deprecated Array.data_zipWith]

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

Alias of Array.data_zipWith.

theorem Array.size_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : α → β → γ) : (as.zipWith bs f).size = min as.size bs.size

theorem Array.data_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) : (as.zip bs).data = as.data.zip bs.data

@[deprecated Array.data_zip]

theorem Array.zip_eq_zip_data {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) : (as.zip bs).data = as.data.zip bs.data

Alias of Array.data_zip.

theorem Array.size_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) : (as.zip bs).size = min as.size bs.size

filter

theorem Array.size_filter_le {α : Type u_1} (p : α → Bool) (l : Array α) : (Array.filter p l).size ≤ l.size

join

@[simp]

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

@[deprecated Array.data_join]

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

Alias of Array.data_join.

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

erase

shrink

theorem Array.size_shrink_loop {α : Type u_1} (a : Array α) (n : Nat) : (Array.shrink.loop n a).size = a.size - n

theorem Array.size_shrink {α : Type u_1} (a : Array α) (n : Nat) : (a.shrink n).size = min a.size n

set

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

map

theorem Array.mapM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : Array.mapM f #[] = pure #[]

@[simp]

theorem Array.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) : Array.map f #[] = #[]

mem

theorem Array.not_mem_empty {α : Type u_1} (a : α) : ¬a ∈ #[]

Alias of Array.not_mem_nil.

theorem Array.mem_singleton : ∀ {α : Type u_1} {b a : α}, a ∈ #[b] ↔ a = b

append

theorem Array.append_empty {α : Type u_1} (as : Array α) : as ++ #[] = as

Alias of Array.append_nil.

theorem Array.empty_append {α : Type u_1} (as : Array α) : #[] ++ as = as

Alias of Array.nil_append.

insertAt

theorem Array.size_insertAt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) : (as.insertAt i v).size = as.size + 1

theorem Array.getElem_insertAt_lt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) (k : Nat) (hlt : k < ↑i) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} : (as.insertAt i v)[k] = as[k]

theorem Array.getElem_insertAt_gt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) (k : Nat) (hgt : k > ↑i) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} : (as.insertAt i v)[k] = as[k - 1]

theorem Array.getElem_insertAt_eq {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) (k : Nat) (heq : ↑i = k) {hk : k < (as.insertAt i v).size} : (as.insertAt i v)[k] = v