mathlib documentation

core / data.vector

def vector (α : Type u) (n : ) :
Type u
Equations
@[protected, instance]
def vector.decidable_eq {α : Type u} {n : } [decidable_eq α] :
Equations
def vector.nil {α : Type u} :
vector α 0
Equations
def vector.cons {α : Type u} {n : } :
α → vector α nvector α n.succ
Equations
def vector.length {α : Type u} {n : } (v : vector α n) :
Equations
def vector.head {α : Type u} {n : } :
vector α n.succ → α
Equations
@[simp]
theorem vector.head_cons {α : Type u} {n : } (a : α) (v : vector α n) :
(a::ᵥv).head = a
def vector.tail {α : Type u} {n : } :
vector α nvector α (n - 1)
Equations
@[simp]
theorem vector.tail_cons {α : Type u} {n : } (a : α) (v : vector α n) :
(a::ᵥv).tail = v
@[simp]
theorem vector.cons_head_tail {α : Type u} {n : } (v : vector α n.succ) :
def vector.to_list {α : Type u} {n : } (v : vector α n) :
list α
Equations
def vector.nth {α : Type u} {n : } (v : vector α n) :
fin n → α
Equations
def vector.append {α : Type u} {n m : } :
vector α nvector α mvector α (n + m)
Equations
def vector.elim {α : Type u_1} {C : Π {n : }, vector α nSort u} (H : Π (l : list α), C l, _⟩) {n : } (v : vector α n) :
C v
Equations
def vector.map {α : Type u} {β : Type v} {n : } (f : α → β) :
vector α nvector β n
Equations
@[simp]
theorem vector.map_nil {α : Type u} {β : Type v} (f : α → β) :
theorem vector.map_cons {α : Type u} {β : Type v} {n : } (f : α → β) (a : α) (v : vector α n) :
def vector.map₂ {α : Type u} {β : Type v} {φ : Type w} {n : } (f : α → β → φ) :
vector α nvector β nvector φ n
Equations
def vector.repeat {α : Type u} (a : α) (n : ) :
vector α n
Equations
def vector.drop {α : Type u} {n : } (i : ) :
vector α nvector α (n - i)
Equations
def vector.take {α : Type u} {n : } (i : ) :
vector α nvector α (min i n)
Equations
def vector.remove_nth {α : Type u} {n : } (i : fin n) :
vector α nvector α (n - 1)
Equations
def vector.of_fn {α : Type u} {n : } :
(fin n → α)vector α n
Equations
def vector.map_accumr {α : Type u} {β : Type v} {n : } {σ : Type} (f : α → σ → σ × β) :
vector α nσ → σ × vector β n
Equations
def vector.map_accumr₂ {n : } {α β σ φ : Type} (f : α → β → σ → σ × φ) :
vector α nvector β nσ → σ × vector φ n
Equations
@[protected]
theorem vector.eq {α : Type u} {n : } (a1 a2 : vector α n) :
a1.to_list = a2.to_lista1 = a2
@[protected]
theorem vector.eq_nil {α : Type u} (v : vector α 0) :
@[simp]
theorem vector.to_list_mk {α : Type u} {n : } (v : list α) (P : v.length = n) :
@[simp]
theorem vector.to_list_nil {α : Type u} :
@[simp]
theorem vector.to_list_length {α : Type u} {n : } (v : vector α n) :
@[simp]
theorem vector.to_list_cons {α : Type u} {n : } (a : α) (v : vector α n) :
@[simp]
theorem vector.to_list_append {α : Type u} {n m : } (v : vector α n) (w : vector α m) :
@[simp]
theorem vector.to_list_drop {α : Type u} {n m : } (v : vector α m) :
@[simp]
theorem vector.to_list_take {α : Type u} {n m : } (v : vector α m) :