@[instance]
Equations
theorem
array.rev_list_reverse_aux
{n : ℕ}
{α : Type u}
{a : array n α}
(i : ℕ)
(h : i ≤ n)
(t : list α) :
(d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil).reverse_core t = d_array.rev_iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h t
theorem
array.rev_list_foldr_aux
{n : ℕ}
{α : Type u}
{β : Type w}
{b : β}
{f : α → β → β}
{a : array n α}
{i : ℕ}
(h : i ≤ n) :
list.foldr f b (d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil) = d_array.iterate_aux a (λ (_x : fin n), f) i h b
theorem
array.rev_list_foldr
{n : ℕ}
{α : Type u}
{β : Type w}
{b : β}
{f : α → β → β}
{a : array n α} :
list.foldr f b a.rev_list = a.foldl b f
theorem
array.to_list_foldl
{n : ℕ}
{α : Type u}
{β : Type w}
{b : β}
{f : β → α → β}
{a : array n α} :
list.foldl f b a.to_list = a.foldl b (function.swap f)
@[simp]
theorem
array.read_map₂
{n : ℕ}
{α : Type u}
{i : fin n}
{f : α → α → α}
{a₁ a₂ : array n α} :
(array.map₂ f a₁ a₂).read i = f (a₁.read i) (a₂.read i)
Equations
- equiv.d_array_equiv_fin α = {to_fun := d_array.read α, inv_fun := d_array.mk (λ (i : fin n), α i), left_inv := _, right_inv := _}
Equations
- equiv.array_equiv_fin n α = equiv.d_array_equiv_fin (λ (_x : fin n), α)
Equations
- equiv.vector_equiv_fin α n = {to_fun := vector.nth n, inv_fun := vector.of_fn n, left_inv := _, right_inv := _}
Equations
- equiv.vector_equiv_array α n = (equiv.vector_equiv_fin α n).trans (equiv.array_equiv_fin n α).symm
@[instance]
Equations
- array.traversable = equiv.traversable (λ (α : Type u_1), equiv.vector_equiv_array α n)
@[instance]
Equations
- array.is_lawful_traversable = equiv.is_lawful_traversable (λ (α : Type u_1), equiv.vector_equiv_array α n)