core / data.vector - scilib docs

source

def vector (α : Type u) (n : ℕ) :

Type u

Equations

vector α n = {l // l.length = n}

Instances for vector

source

@[protected, instance]

def vector.decidable_eq {α : Type u} {n : ℕ} [decidable_eq α] :

decidable_eq (vector α n)

Equations

vector.decidable_eq = vector.decidable_eq._proof_1.mpr (λ (a b : {l // l.length = n}), subtype.decidable_eq a b)

source

def vector.nil {α : Type u} :

vector α 0

Equations

vector.nil = ⟨list.nil α, _⟩

source

def vector.cons {α : Type u} {n : ℕ} :

α → vector α n → vector α n.succ

Equations

a ::ᵥ ⟨v, h⟩ = ⟨a :: v, _⟩

source

@[reducible]

def vector.length {α : Type u} {n : ℕ} (v : vector α n) :

ℕ

Equations

v.length = n

source

def vector.head {α : Type u} {n : ℕ} :

vector α n.succ → α

Equations

vector.head ⟨a :: v, h⟩ = a
vector.head ⟨list.nil α, h⟩ = nat.no_confusion h

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

vector.tail ⟨a :: v, h⟩ = ⟨v, _⟩
vector.tail ⟨list.nil α, h⟩ = ⟨list.nil α, _⟩

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

v.to_list = v.val

source

def vector.nth {α : Type u} {n : ℕ} (v : vector α n) :

fin n → α

Equations

vector.nth ⟨l, h⟩ i = l.nth_le i.val _

source

def vector.append {α : Type u} {n m : ℕ} :

vector α n → vector α m → vector α (n + m)

Equations

vector.append ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ = ⟨l₁ ++ l₂, _⟩

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

vector.elim H ⟨l, h⟩ = vector.elim._match_1 H l n h
vector.elim._match_1 H l l.length rfl = H l

source

def vector.map {α : Type u} {β : Type v} {n : ℕ} (f : α → β) :

vector α n → vector β n

Equations

vector.map f ⟨l, h⟩ = ⟨list.map f l, _⟩

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

vector.map₂ f ⟨x, _x⟩ ⟨y, _x_1⟩ = ⟨list.map₂ f x y, _⟩

source

def vector.repeat {α : Type u} (a : α) (n : ℕ) :

vector α n

Equations

vector.repeat a n = ⟨list.repeat a n, _⟩

source

def vector.drop {α : Type u} {n : ℕ} (i : ℕ) :

vector α n → vector α (n - i)

Equations

vector.drop i ⟨l, p⟩ = ⟨list.drop i l, _⟩

source

def vector.take {α : Type u} {n : ℕ} (i : ℕ) :

vector α n → vector α (linear_order.min i n)

Equations

vector.take i ⟨l, p⟩ = ⟨list.take i l, _⟩

source

def vector.remove_nth {α : Type u} {n : ℕ} (i : fin n) :

vector α n → vector α (n - 1)

Equations

vector.remove_nth i ⟨l, p⟩ = ⟨l.remove_nth i.val, _⟩

source

def vector.of_fn {α : Type u} {n : ℕ} :

(fin n → α) → vector α n

Equations

vector.of_fn f = f 0 ::ᵥ vector.of_fn (λ (i : fin n), f i.succ)
vector.of_fn f = vector.nil

source

def vector.map_accumr {α : Type u} {β : Type v} {n : ℕ} {σ : Type} (f : α → σ → σ × β) :

vector α n → σ → σ × vector β n

Equations

vector.map_accumr f ⟨x, px⟩ c = let res : σ × list β := list.map_accumr f x c in (res.fst, ⟨res.snd, _⟩)

source

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

vector α n → vector β n → σ → σ × vector φ n

Equations

vector.map_accumr₂ f ⟨x, px⟩ ⟨y, py⟩ c = let res : σ × list φ := list.map_accumr₂ f x y c in (res.fst, ⟨res.snd, _⟩)

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