mathlib documentation

core.data.vector

def vector  :
Type uType u

Equations
@[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 : } :
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 : } :
vector α nlist α

Equations
def vector.nth {α : Type u} {n : } :
vector α nfin 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 : } :
(α → β)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 : } :
(α → β → φ)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 : } :
fin nvector α 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} :
(α → σ → σ × β)vector α nσ → σ × vector β n

Equations
def vector.map_accumr₂ {n : } {α β σ φ : Type} :
(α → β → σ → σ × φ)vector α nvector β nσ → σ × vector φ n

Equations
theorem vector.eq {α : Type u} {n : } (a1 a2 : vector α n) :
a1.to_list = a2.to_lista1 = a2

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) :