@[instance]
Equations
- vector.inhabited = {default := vector.of_fn (λ (_x : fin n), inhabited.default α)}
@[simp]
theorem
vector.to_list_of_fn
{α : Type u_1}
{n : ℕ}
(f : fin n → α) :
(vector.of_fn f).to_list = list.of_fn f
@[simp]
theorem
vector.to_list_map
{n : ℕ}
{α : Type u_1}
{β : Type u_2}
(v : vector α n)
(f : α → β) :
(vector.map f v).to_list = list.map f v.to_list
@[simp]
theorem
vector.nth_map
{n : ℕ}
{α : Type u_1}
{β : Type u_2}
(v : vector α n)
(f : α → β)
(i : fin n) :
(vector.map f v).nth i = f (v.nth i)
@[simp]
theorem
vector.nth_of_fn
{α : Type u_1}
{n : ℕ}
(f : fin n → α)
(i : fin n) :
(vector.of_fn f).nth i = f i
@[simp]
@[simp]
theorem
vector.tail_of_fn
{α : Type u_1}
{n : ℕ}
(f : fin n.succ → α) :
(vector.of_fn f).tail = vector.of_fn (λ (i : fin (n.succ - 1)), f i.succ)
theorem
vector.head'_to_list
{n : ℕ}
{α : Type u_1}
(v : vector α n.succ) :
v.to_list.head' = option.some v.head
@[simp]
theorem
vector.head_of_fn
{α : Type u_1}
{n : ℕ}
(f : fin n.succ → α) :
(vector.of_fn f).head = f 0
Equations
- vector.m_of_fn f = f 0 >>= λ (a : α), vector.m_of_fn (λ (i : fin n), f i.succ) >>= λ (v : vector α n), has_pure.pure (a :: v)
- vector.m_of_fn f = has_pure.pure vector.nil
theorem
vector.m_of_fn_pure
{m : Type u_1 → Type u_2}
[monad m]
[is_lawful_monad m]
{α : Type u_1}
{n : ℕ}
(f : fin n → α) :
vector.m_of_fn (λ (i : fin n), has_pure.pure (f i)) = has_pure.pure (vector.of_fn f)
def
vector.mmap
{m : Type u → Type u_1}
[monad m]
{α : Type u_2}
{β : Type u}
(f : α → m β)
{n : ℕ} :
Equations
- vector.mmap f ⟨a :: l, _⟩ = f a >>= λ (h' : β), vector.mmap f ⟨l, _⟩ >>= λ (t' : vector β l.length), has_pure.pure (h' :: t')
- vector.mmap f ⟨list.nil α, _⟩ = has_pure.pure vector.nil
@[simp]
theorem
vector.mmap_nil
{m : Type u_1 → Type u_2}
[monad m]
{α : Type u_3}
{β : Type u_1}
(f : α → m β) :
@[simp]
theorem
vector.mmap_cons
{m : Type u_1 → Type u_2}
[monad m]
{α : Type u_3}
{β : Type u_1}
(f : α → m β)
(a : α)
{n : ℕ}
(v : vector α n) :
vector.mmap f (a :: v) = f a >>= λ (h' : β), vector.mmap f v >>= λ (t' : vector β n), has_pure.pure (h' :: t')
@[instance]
Equations
Equations
- vector.to_array ⟨xs, h⟩ = cast _ xs.to_array
Equations
- vector.insert_nth a i v = ⟨list.insert_nth i.val a v.val, _⟩
theorem
vector.insert_nth_val
{n : ℕ}
{α : Type u_1}
{a : α}
{i : fin (n + 1)}
{v : vector α n} :
(vector.insert_nth a i v).val = list.insert_nth i.val a v.val
@[simp]
theorem
vector.remove_nth_val
{n : ℕ}
{α : Type u_1}
{i : fin n}
{v : vector α n} :
(vector.remove_nth i v).val = v.val.remove_nth i.val
theorem
vector.remove_nth_insert_nth
{n : ℕ}
{α : Type u_1}
{a : α}
{v : vector α n}
{i : fin (n + 1)} :
vector.remove_nth i (vector.insert_nth a i v) = v
theorem
vector.remove_nth_insert_nth_ne
{n : ℕ}
{α : Type u_1}
{a : α}
{v : vector α (n + 1)}
{i j : fin (n + 2)}
(h : i ≠ j) :
vector.remove_nth i (vector.insert_nth a j v) = vector.insert_nth a (i.pred_above j _) (vector.remove_nth (j.pred_above i h) v)
theorem
vector.insert_nth_comm
{n : ℕ}
{α : Type u_1}
(a b : α)
(i j : fin (n + 1))
(h : i ≤ j)
(v : vector α n) :
vector.insert_nth b j.succ (vector.insert_nth a i v) = vector.insert_nth a i.cast_succ (vector.insert_nth b j v)
update_nth v n a replaces the nth element of v with a
Equations
- v.update_nth i a = ⟨v.val.update_nth i.val a, _⟩
@[simp]
theorem
vector.nth_update_nth_same
{n : ℕ}
{α : Type u_1}
(v : vector α n)
(i : fin n)
(a : α) :
(v.update_nth i a).nth i = a
theorem
vector.nth_update_nth_of_ne
{n : ℕ}
{α : Type u_1}
{v : vector α n}
{i j : fin n}
(h : i ≠ j)
(a : α) :
(v.update_nth i a).nth j = v.nth j
Equations
- vector.traverse f ⟨v, Hv⟩ = cast _ (traverse_aux f v)
@[simp]
theorem
vector.traverse_def
{n : ℕ}
{F : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
{α β : Type u}
(f : α → F β)
(x : α)
(xs : vector α n) :
vector.traverse f (x :: xs) = vector.cons <$> f x <*> vector.traverse f xs
theorem
vector.comp_traverse
{n : ℕ}
{F G : Type u → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
{α β γ : Type u}
(f : β → F γ)
(g : α → G β)
(x : vector α n) :
vector.traverse (functor.comp.mk ∘ functor.map f ∘ g) x = functor.comp.mk (vector.traverse f <$> vector.traverse g x)
theorem
vector.traverse_eq_map_id
{n : ℕ}
{α β : Type u_1}
(f : α → β)
(x : vector α n) :
vector.traverse (id.mk ∘ f) x = id.mk (vector.map f x)
theorem
vector.naturality
{n : ℕ}
{F G : Type u → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
(η : applicative_transformation F G)
{α β : Type u}
(f : α → F β)
(x : vector α n) :
⇑η (vector.traverse f x) = vector.traverse (⇑η ∘ f) x
@[instance]
Equations
- vector.traversable = {to_functor := {map := λ (α β : Type u), vector.map, map_const := λ (α β : Type u), vector.map ∘ function.const β}, traverse := vector.traverse n}
@[instance]
Equations
- vector.is_lawful_traversable = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}