core / data.vector - mathlib3 docs

mathlib3 documentation

core / data.vector

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