@[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 β))
:
Alias of Array.forIn_eq_forIn_toList
.
Alias of Array.forIn_eq_forIn_toList
.
zipWith / zip #
theorem
Array.toList_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(as : Array α)
(bs : Array β)
:
(as.zipWith bs f).toList = List.zipWith f as.toList bs.toList
@[irreducible]
@[deprecated Array.toList_zipWith]
theorem
Array.data_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(as : Array α)
(bs : Array β)
:
(as.zipWith bs f).toList = List.zipWith f as.toList bs.toList
Alias of Array.toList_zipWith
.
@[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).toList = List.zipWith f as.toList bs.toList
Alias of Array.toList_zipWith
.
Alias of Array.toList_zipWith
.
@[deprecated Array.toList_zip]
theorem
Array.data_zip
{α : Type u_1}
{β : Type u_2}
(as : Array α)
(bs : Array β)
:
(as.zip bs).toList = as.toList.zip bs.toList
Alias of Array.toList_zip
.
@[deprecated Array.data_zip]
theorem
Array.zip_eq_zip_data
{α : Type u_1}
{β : Type u_2}
(as : Array α)
(bs : Array β)
:
(as.zip bs).toList = as.toList.zip bs.toList
Alias of Array.toList_zip
.
Alias of Array.toList_zip
.
filter #
theorem
Array.size_filter_le
{α : Type u_1}
(p : α → Bool)
(l : Array α)
:
(Array.filter p l).size ≤ l.size
join #
@[deprecated Array.toList_join]
Alias of Array.toList_join
.
@[deprecated Array.data_join]
Alias of Array.toList_join
.
Alias of Array.toList_join
.
indexOf? #
theorem
Array.indexOf?_toList
{α : Type u_1}
[BEq α]
{a : α}
{l : Array α}
:
List.indexOf? a l.toList = Option.map Fin.val (l.indexOf? a)
@[irreducible]
theorem
Array.indexOf?_toList.aux
{α : Type u_1}
[BEq α]
{a : α}
(l : Array α)
(i : Nat)
:
Option.map (fun (x : Nat) => x + i) (List.indexOf? a (List.drop i l.toList)) = Option.map Fin.val (l.indexOfAux a i)
erase #
shrink #
theorem
Array.size_shrink_loop
{α : Type u_1}
(a : Array α)
(n : Nat)
:
(Array.shrink.loop n a).size = a.size - n
set #
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 #[]
mem #
append #
Alias of Array.append_nil
.
Alias of Array.nil_append
.