mathlib3 documentation

core / data.vector

@[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 α n vector α n.succ
Equations
@[reducible]
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 α n vector α (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 α n vector α m vector α (n + m)
Equations
def vector.elim {α : Type u_1} {C : Π {n : }, vector α n Sort u} (H : Π (l : list α), C l, _⟩) {n : } (v : vector α n) :
C v
Equations
def vector.map {α : Type u} {β : Type v} {n : } (f : α β) :
vector α n vector β 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 α n vector β n vector φ n
Equations
def vector.repeat {α : Type u} (a : α) (n : ) :
vector α n
Equations
def vector.drop {α : Type u} {n : } (i : ) :
vector α n vector α (n - i)
Equations
def vector.take {α : Type u} {n : } (i : ) :
Equations
def vector.remove_nth {α : Type u} {n : } (i : fin n) :
vector α n vector α (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 α n vector β n σ σ × vector φ n
Equations
@[protected]
theorem vector.eq {α : Type u} {n : } (a1 a2 : vector α n) :
a1.to_list = a2.to_list a1 = 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]
@[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) :