Documentation

Batteries.Data.Array.Lemmas

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
theorem Array.forIn_eq_data_forIn.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.sizeArray.forIn.loop as f i h b = forIn (List.drop j as.data) b f

zipWith / zip #

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
@[irreducible]
theorem Array.zipWith_eq_zipWith_data.loop {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :
i as.sizei 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)
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.zip_eq_zip_data {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :
(as.zip bs).data = as.data.zip bs.data
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 0).size l.size

join #

@[simp]
theorem Array.join_data {α : Type u_1} {l : Array (Array α)} :
l.join.data = (List.map Array.data l.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