mathlib3 documentation

data.vector.basic

Additional theorems and definitions about the vector type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file introduces the infix notation ::ᵥ for vector.cons.

source
@[protected, instance]
def vector.inhabited {n : ℕ} {α : Type u_1} [inhabited α] :
inhabited (vector α n)
Equations
source
theorem vector.to_list_injective {n : ℕ} {α : Type u_1} :
function.injective vector.to_list
source
@[ext]
theorem vector.ext {n : ℕ} {α : Type u_1} {v w : vector α n} (h : ∀ (m : fin n), v.nth m = w.nth m) :
v = w

Two v w : vector α n are equal iff they are equal at every single index.

source
def vector.replicate {α : Type u_1} (n : ℕ) (a : α) :
vector α n

A vector with n elements a.

Equations
source
@[protected, instance]
def vector.zero_subsingleton {α : Type u_1} :
subsingleton (vector α 0)

The empty vector is a subsingleton.

source
@[simp]
theorem vector.cons_val {n : ℕ} {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).val = a :: v.val
source
@[simp]
theorem vector.cons_head {n : ℕ} {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).head = a
source
@[simp]
theorem vector.cons_tail {n : ℕ} {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).tail = v
source
theorem vector.eq_cons_iff {n : ℕ} {α : Type u_1} (a : α) (v : vector α n.succ) (v' : vector α n) :
v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v'
source
theorem vector.ne_cons_iff {n : ℕ} {α : Type u_1} (a : α) (v : vector α n.succ) (v' : vector α n) :
v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
source
theorem vector.exists_eq_cons {n : ℕ} {α : Type u_1} (v : vector α n.succ) :
∃ (a : α) (as : vector α n), v = a ::ᵥ as
source
@[simp]
theorem vector.to_list_of_fn {α : Type u_1} {n : ℕ} (f : fin n → α) :
(vector.of_fn f).to_list = list.of_fn f
source
@[simp]
theorem vector.mk_to_list {n : ℕ} {α : Type u_1} (v : vector α n) (h : v.to_list.length = n) :
⟨v.to_list, h⟩ = v
source
@[simp]
theorem vector.length_coe {n : ℕ} {α : Type u_1} (v : vector α n) :
↑v.length = n
source
@[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
source
@[simp]
theorem vector.head_map {n : ℕ} {α : Type u_1} {β : Type u_2} (v : vector α (n + 1)) (f : α → β) :
(vector.map f v).head = f v.head
source
@[simp]
theorem vector.tail_map {n : ℕ} {α : Type u_1} {β : Type u_2} (v : vector α (n + 1)) (f : α → β) :
(vector.map f v).tail = vector.map f v.tail
source
theorem vector.nth_eq_nth_le {n : ℕ} {α : Type u_1} (v : vector α n) (i : fin n) :
v.nth i = v.to_list.nth_le i.val _
source
@[simp]
theorem vector.nth_replicate {n : ℕ} {α : Type u_1} (a : α) (i : fin n) :
(vector.replicate n a).nth i = a
source
@[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)
source
@[simp]
theorem vector.nth_of_fn {α : Type u_1} {n : ℕ} (f : fin n → α) (i : fin n) :
(vector.of_fn f).nth i = f i
source
@[simp]
theorem vector.of_fn_nth {n : ℕ} {α : Type u_1} (v : vector α n) :
vector.of_fn v.nth = v
source
def equiv.vector_equiv_fin (α : Type u_1) (n : ℕ) :
vector α n ≃ (fin n → α)

The natural equivalence between length-n vectors and functions from fin n.

Equations
source
theorem vector.nth_tail {n : ℕ} {α : Type u_1} (x : vector α n) (i : fin (n - 1)) :
x.tail.nth i = x.nth ⟨i.val + 1, _⟩
source
@[simp]
theorem vector.nth_tail_succ {n : ℕ} {α : Type u_1} (v : vector α n.succ) (i : fin n) :
v.tail.nth i = v.nth i.succ
source
@[simp]
theorem vector.tail_val {n : ℕ} {α : Type u_1} (v : vector α n.succ) :
v.tail.val = v.val.tail
source
@[simp]
theorem vector.tail_nil {α : Type u_1} :
vector.nil.tail = vector.nil

The tail of a nil vector is nil.

source
@[simp]
theorem vector.singleton_tail {α : Type u_1} (v : vector α 1) :
v.tail = vector.nil

The tail of a vector made up of one element is nil.

source
@[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)
source
@[simp]
theorem vector.to_list_empty {α : Type u_1} (v : vector α 0) :
v.to_list = list.nil
source
@[simp]
theorem vector.to_list_singleton {α : Type u_1} (v : vector α 1) :
v.to_list = [v.head]

The list that makes up a vector made up of a single element, retrieved via to_list, is equal to the list of that single element.

source
@[simp]
theorem vector.empty_to_list_eq_ff {n : ℕ} {α : Type u_1} (v : vector α (n + 1)) :
v.to_list.empty = bool.ff
source
theorem vector.not_empty_to_list {n : ℕ} {α : Type u_1} (v : vector α (n + 1)) :
¬↥(v.to_list.empty)
source
@[simp]
theorem vector.map_id {α : Type u_1} {n : ℕ} (v : vector α n) :
vector.map id v = v

Mapping under id does not change a vector.

source
theorem vector.nodup_iff_nth_inj {n : ℕ} {α : Type u_1} {v : vector α n} :
v.to_list.nodup ↔ function.injective v.nth
source
theorem vector.head'_to_list {n : ℕ} {α : Type u_1} (v : vector α n.succ) :
v.to_list.head' = option.some v.head
source
def vector.reverse {n : ℕ} {α : Type u_1} (v : vector α n) :
vector α n

Reverse a vector.

Equations
source
theorem vector.to_list_reverse {n : ℕ} {α : Type u_1} {v : vector α n} :
v.reverse.to_list = v.to_list.reverse

The list of a vector after a reverse, retrieved by to_list is equal to the list.reverse after retrieving a vector's to_list.

source
@[simp]
theorem vector.reverse_reverse {n : ℕ} {α : Type u_1} {v : vector α n} :
v.reverse.reverse = v
source
@[simp]
theorem vector.nth_zero {n : ℕ} {α : Type u_1} (v : vector α n.succ) :
v.nth 0 = v.head
source
@[simp]
theorem vector.head_of_fn {α : Type u_1} {n : ℕ} (f : fin n.succ → α) :
(vector.of_fn f).head = f 0
source
@[simp]
theorem vector.nth_cons_zero {n : ℕ} {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).nth 0 = a
source
@[simp]
theorem vector.nth_cons_nil {α : Type u_1} {ix : fin 1} (x : α) :
(x ::ᵥ vector.nil).nth ix = x

Accessing the nth element of a vector made up of one element x : α is x itself.

source
@[simp]
theorem vector.nth_cons_succ {n : ℕ} {α : Type u_1} (a : α) (v : vector α n) (i : fin n) :
(a ::ᵥ v).nth i.succ = v.nth i
source
def vector.last {n : ℕ} {α : Type u_1} (v : vector α (n + 1)) :
α

The last element of a vector, given that the vector is at least one element.

Equations
source
theorem vector.last_def {n : ℕ} {α : Type u_1} {v : vector α (n + 1)} :
v.last = v.nth (fin.last n)

The last element of a vector, given that the vector is at least one element.

source
theorem vector.reverse_nth_zero {n : ℕ} {α : Type u_1} {v : vector α (n + 1)} :
v.reverse.head = v.last

The last element of a vector is the head of the reverse vector.

source
def vector.scanl {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α n) :
vector β (n + 1)

Construct a vector β (n + 1) from a vector α n by scanning f : β → α → β from the "left", that is, from 0 to fin.last n, using b : β as the starting value.

Equations
source
@[simp]
theorem vector.scanl_nil {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) :
vector.scanl f b vector.nil = b ::ᵥ vector.nil

Providing an empty vector to scanl gives the starting value b : β.

source
@[simp]
theorem vector.scanl_cons {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α n) (x : α) :
vector.scanl f b (x ::ᵥ v) = b ::ᵥ vector.scanl f (f b x) v

The recursive step of scanl splits a vector x ::ᵥ v : vector α (n + 1) into the provided starting value b : β and the recursed scanl f b x : β as the starting value.

This lemma is the cons version of scanl_nth.

source
@[simp]
theorem vector.scanl_val {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) {v : vector α n} :
(vector.scanl f b v).val = list.scanl f b v.val

The underlying list of a vector after a scanl is the list.scanl of the underlying list of the original vector.

source
@[simp]
theorem vector.to_list_scanl {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α n) :
(vector.scanl f b v).to_list = list.scanl f b v.to_list

The to_list of a vector after a scanl is the list.scanl of the to_list of the original vector.

source
@[simp]
theorem vector.scanl_singleton {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α 1) :
vector.scanl f b v = b ::ᵥ f b v.head ::ᵥ vector.nil

The recursive step of scanl splits a vector made up of a single element x ::ᵥ nil : vector α 1 into a vector of the provided starting value b : β and the mapped f b x : β as the last value.

source
@[simp]
theorem vector.scanl_head {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α n) :
(vector.scanl f b v).head = b

The first element of scanl of a vector v : vector α n, retrieved via head, is the starting value b : β.

source
@[simp]
theorem vector.scanl_nth {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α n) (i : fin n) :
(vector.scanl f b v).nth i.succ = f ((vector.scanl f b v).nth (⇑fin.cast_succ i)) (v.nth i)

For an index i : fin n, the nth element of scanl of a vector v : vector α n at i.succ, is equal to the application function f : β → α → β of the i.cast_succ element of scanl f b v and nth v i.

This lemma is the nth version of scanl_cons.

source
def vector.m_of_fn {m : Type u → Type u_1} [monad m] {α : Type u} {n : ℕ} :
(fin n → m α) → m (vector α n)

Monadic analog of vector.of_fn. Given a monadic function on fin n, return a vector α n inside the monad.

Equations
source
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)
source
def vector.mmap {m : Type u → Type u_1} [monad m] {α : Type u_2} {β : Type u} (f : α → m β) {n : ℕ} :
vector α n → m (vector β n)

Apply a monadic function to each component of a vector, returning a vector inside the monad.

Equations
source
@[simp]
theorem vector.mmap_nil {m : Type u_1 → Type u_2} [monad m] {α : Type u_3} {β : Type u_1} (f : α → m β) :
vector.mmap f vector.nil = has_pure.pure vector.nil
source
@[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')
source
def vector.induction_on {α : Type u_1} {C : Π {n : ℕ}, vector α n → Sort u_2} {n : ℕ} (v : vector α n) (h_nil : C vector.nil) (h_cons : Π {n : ℕ} {x : α} {w : vector α n}, C w → C (x ::ᵥ w)) :
C v

Define C v by induction on v : vector α n.

This function has two arguments: h_nil handles the base case on C nil, and h_cons defines the inductive step using ∀ x : α, C w → C (x ::ᵥ w).

This can be used as induction v using vector.induction_on.

Equations
  • v.induction_on h_nil h_cons = nat.rec (λ (v : vector α 0), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = 0), v_val.cases_on (λ (v_property : list.nil.length = 0), v_property.dcases_on (λ (a : 0 = 0) (H_2 : v_property == vector.induction_on._proof_1), h_nil) _ _) (λ (v_val_hd : α) (v_val_tl : list α) (v_property : (v_val_hd :: v_val_tl).length = 0), v_property.dcases_on (λ (a : 0 = (v_val_tl.length.add 0).succ), nat.no_confusion a) _ _) v_property)) (λ (n : ℕ) (ih : Π (v : vector α n), C v) (v : vector α n.succ), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = n.succ), v_val.cases_on (λ (v_property : list.nil.length = n.succ), v_property.dcases_on (λ (a : n.succ = 0), nat.no_confusion a) _ _) (λ (a : α) (v : list α) (v_property : (a :: v).length = n.succ), h_cons (ih ⟨v, _⟩)) v_property)) n v
source
def vector.induction_on₂ {n : ℕ} {α : Type u_1} {β : Type u_2} {C : Π {n : ℕ}, vector α n → vector β n → Sort u_3} (v : vector α n) (w : vector β n) (h_nil : C vector.nil vector.nil) (h_cons : Π {n : ℕ} {a : α} {b : β} {x : vector α n} {y : vector β n}, C x y → C (a ::ᵥ x) (b ::ᵥ y)) :
C v w

Define C v w by induction on a pair of vectors v : vector α n and w : vector β n.

Equations
  • v.induction_on₂ w h_nil h_cons = nat.rec (λ (v : vector α 0) (w : vector β 0), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = 0), v_val.cases_on (λ (v_property : list.nil.length = 0), v_property.dcases_on (λ (a : 0 = 0) (H_2 : v_property == vector.induction_on₂._proof_1), subtype.cases_on w (λ (w_val : list β) (w_property : w_val.length = 0), w_val.cases_on (λ (w_property : list.nil.length = 0), w_property.dcases_on (λ (a : 0 = 0) (H_2 : w_property == vector.induction_on₂._proof_2), h_nil) _ _) (λ (w_val_hd : β) (w_val_tl : list β) (w_property : (w_val_hd :: w_val_tl).length = 0), w_property.dcases_on (λ (a : 0 = (w_val_tl.length.add 0).succ), nat.no_confusion a) _ _) w_property)) _ _) (λ (v_val_hd : α) (v_val_tl : list α) (v_property : (v_val_hd :: v_val_tl).length = 0), v_property.dcases_on (λ (a : 0 = (v_val_tl.length.add 0).succ), nat.no_confusion a) _ _) v_property)) (λ (n : ℕ) (ih : Π (v : vector α n) (w : vector β n), C v w) (v : vector α n.succ) (w : vector β n.succ), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = n.succ), v_val.cases_on (λ (v_property : list.nil.length = n.succ), v_property.dcases_on (λ (a : n.succ = 0), nat.no_confusion a) _ _) (λ (a : α) (v : list α) (v_property : (a :: v).length = n.succ), subtype.cases_on w (λ (w_val : list β) (w_property : w_val.length = n.succ), w_val.cases_on (λ (w_property : list.nil.length = n.succ), w_property.dcases_on (λ (a_1 : n.succ = 0), nat.no_confusion a_1) _ _) (λ (b : β) (w : list β) (w_property : (b :: w).length = n.succ), h_cons (ih ⟨v, _⟩ ⟨w, _⟩)) w_property)) v_property)) n v w
source
def vector.induction_on₃ {n : ℕ} {α : Type u_1} {β : Type u_2} {γ : Type u_3} {C : Π {n : ℕ}, vector α n → vector β n → vector γ n → Sort u_4} (u : vector α n) (v : vector β n) (w : vector γ n) (h_nil : C vector.nil vector.nil vector.nil) (h_cons : Π {n : ℕ} {a : α} {b : β} {c : γ} {x : vector α n} {y : vector β n} {z : vector γ n}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) :
C u v w

Define C u v w by induction on a triplet of vectors u : vector α n, v : vector β n, and w : vector γ b.

Equations
  • u.induction_on₃ v w h_nil h_cons = nat.rec (λ (u : vector α 0) (v : vector β 0) (w : vector γ 0), subtype.cases_on u (λ (u_val : list α) (u_property : u_val.length = 0), u_val.cases_on (λ (u_property : list.nil.length = 0), u_property.dcases_on (λ (a : 0 = 0) (H_2 : u_property == vector.induction_on₃._proof_1), subtype.cases_on v (λ (v_val : list β) (v_property : v_val.length = 0), v_val.cases_on (λ (v_property : list.nil.length = 0), v_property.dcases_on (λ (a : 0 = 0) (H_2 : v_property == vector.induction_on₃._proof_2), subtype.cases_on w (λ (w_val : list γ) (w_property : w_val.length = 0), w_val.cases_on (λ (w_property : list.nil.length = 0), w_property.dcases_on (λ (a : 0 = 0) (H_2 : w_property == vector.induction_on₃._proof_3), h_nil) _ _) (λ (w_val_hd : γ) (w_val_tl : list γ) (w_property : (w_val_hd :: w_val_tl).length = 0), w_property.dcases_on (λ (a : 0 = (w_val_tl.length.add 0).succ), nat.no_confusion a) _ _) w_property)) _ _) (λ (v_val_hd : β) (v_val_tl : list β) (v_property : (v_val_hd :: v_val_tl).length = 0), v_property.dcases_on (λ (a : 0 = (v_val_tl.length.add 0).succ), nat.no_confusion a) _ _) v_property)) _ _) (λ (u_val_hd : α) (u_val_tl : list α) (u_property : (u_val_hd :: u_val_tl).length = 0), u_property.dcases_on (λ (a : 0 = (u_val_tl.length.add 0).succ), nat.no_confusion a) _ _) u_property)) (λ (n : ℕ) (ih : Π (u : vector α n) (v : vector β n) (w : vector γ n), C u v w) (u : vector α n.succ) (v : vector β n.succ) (w : vector γ n.succ), subtype.cases_on u (λ (u_val : list α) (u_property : u_val.length = n.succ), u_val.cases_on (λ (u_property : list.nil.length = n.succ), u_property.dcases_on (λ (a : n.succ = 0), nat.no_confusion a) _ _) (λ (a : α) (u : list α) (u_property : (a :: u).length = n.succ), subtype.cases_on v (λ (v_val : list β) (v_property : v_val.length = n.succ), v_val.cases_on (λ (v_property : list.nil.length = n.succ), v_property.dcases_on (λ (a_1 : n.succ = 0), nat.no_confusion a_1) _ _) (λ (b : β) (v : list β) (v_property : (b :: v).length = n.succ), subtype.cases_on w (λ (w_val : list γ) (w_property : w_val.length = n.succ), w_val.cases_on (λ (w_property : list.nil.length = n.succ), w_property.dcases_on (λ (a_1 : n.succ = 0), nat.no_confusion a_1) _ _) (λ (c : γ) (w : list γ) (w_property : (c :: w).length = n.succ), h_cons (ih ⟨u, _⟩ ⟨v, _⟩ ⟨w, _⟩)) w_property)) v_property)) u_property)) n u v w
source
def vector.to_array {n : ℕ} {α : Type u_1} :
vector α n → array n α

Cast a vector to an array.

Equations
source
def vector.insert_nth {n : ℕ} {α : Type u_1} (a : α) (i : fin (n + 1)) (v : vector α n) :
vector α (n + 1)

v.insert_nth a i inserts a into the vector v at position i (and shifting later components to the right).

Equations
source
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
source
@[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
source
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
source
theorem vector.remove_nth_insert_nth' {n : ℕ} {α : Type u_1} {a : α} {v : vector α (n + 1)} {i : fin (n + 1)} {j : fin (n + 2)} :
vector.remove_nth (⇑(j.succ_above) i) (vector.insert_nth a j v) = vector.insert_nth a (i.pred_above j) (vector.remove_nth i v)
source
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 (⇑fin.cast_succ i) (vector.insert_nth b j v)
source
def vector.update_nth {n : ℕ} {α : Type u_1} (v : vector α n) (i : fin n) (a : α) :
vector α n

update_nth v n a replaces the nth element of v with a

Equations
source
@[simp]
theorem vector.to_list_update_nth {n : ℕ} {α : Type u_1} (v : vector α n) (i : fin n) (a : α) :
(v.update_nth i a).to_list = v.to_list.update_nth ↑i a
source
@[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
source
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
source
theorem vector.nth_update_nth_eq_if {n : ℕ} {α : Type u_1} {v : vector α n} {i j : fin n} (a : α) :
(v.update_nth i a).nth j = ite (i = j) a (v.nth j)
source
theorem vector.prod_update_nth {n : ℕ} {α : Type u_1} [monoid α] (v : vector α n) (i : fin n) (a : α) :
(v.update_nth i a).to_list.prod = (vector.take ↑i v).to_list.prod * a * (vector.drop (↑i + 1) v).to_list.prod
source
theorem vector.sum_update_nth {n : ℕ} {α : Type u_1} [add_monoid α] (v : vector α n) (i : fin n) (a : α) :
(v.update_nth i a).to_list.sum = (vector.take ↑i v).to_list.sum + a + (vector.drop (↑i + 1) v).to_list.sum
source
theorem vector.sum_update_nth' {n : ℕ} {α : Type u_1} [add_comm_group α] (v : vector α n) (i : fin n) (a : α) :
(v.update_nth i a).to_list.sum = v.to_list.sum + -v.nth i + a
source
theorem vector.prod_update_nth' {n : ℕ} {α : Type u_1} [comm_group α] (v : vector α n) (i : fin n) (a : α) :
(v.update_nth i a).to_list.prod = v.to_list.prod * (v.nth i)⁻¹ * a
source
@[protected]
def vector.traverse {n : ℕ} {F : Type u → Type u} [applicative F] {α β : Type u} (f : α → F β) :
vector α n → F (vector β n)

Apply an applicative function to each component of a vector.

Equations
source
@[protected, simp]
theorem vector.traverse_def {n : ℕ} {F : Type u → Type u} [applicative F] {α β : Type u} (f : α → F β) (x : α) (xs : vector α n) :
vector.traverse f (x ::ᵥ xs) = vector.cons <$> f x <*> vector.traverse f xs
source
@[protected]
theorem vector.id_traverse {n : ℕ} {α : Type u} (x : vector α n) :
vector.traverse id.mk x = x
source
@[protected, nolint]
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)
source
@[protected]
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)
source
@[protected]
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
source
@[protected, instance]
def vector.flip.traversable {n : ℕ} :
traversable (flip vector n)
Equations
source
@[protected, instance]
def vector.flip.is_lawful_traversable {n : ℕ} :
is_lawful_traversable (flip vector n)
Equations
source
@[protected, instance]
meta def vector.reflect [reflected_univ] {α : Type u} [has_reflect α] [reflected (Type u) α] {n : ℕ} :
has_reflect (vector α n)