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]
filter #
theorem
Array.size_filter_le
{α : Type u_1}
(p : α → Bool)
(l : Array α)
:
(Array.filter p l 0).size ≤ l.size
join #
erase #
shrink #
theorem
Array.size_shrink_loop
{α : Type u_1}
(a : Array α)
(n : Nat)
:
(Array.shrink.loop n a).size = a.size - n