# Documentation

Mathlib.Data.Vector

The type Vector represents lists with fixed length.

def Vector (α : Type u) (n : ) :

Vector α n is the type of lists of length n with elements of type α.

Equations
instance Vector.instDecidableEqVector {α : Type u} {n : } [inst : ] :
Equations
@[match_pattern]
def Vector.nil {α : Type u} :
Vector α 0

The empty vector with elements of type α

Equations
• Vector.nil = { val := [], property := (_ : = ) }
@[match_pattern]
def Vector.cons {α : Type u} {n : } :
αVector α nVector α ()

If a : α and l : Vector α n, then cons a l, is the vector of length n + 1 whose first element is a and with l as the rest of the list.

Equations
• = match x, x with | a, { val := v, property := h } => { val := a :: v, property := (_ : = ) }
def Vector.length {α : Type u} {n : } :
Vector α n

The length of a vector.

Equations
def Vector.head {α : Type u} {n : } :
Vector α ()α

The first element of a vector with length at least 1.

Equations
• = match x with | { val := [], property := h } => | { val := a :: tail, property := property } => a
theorem Vector.head_cons {α : Type u} {n : } (a : α) (v : Vector α n) :

The head of a vector obtained by prepending is the element prepended.

def Vector.tail {α : Type u} {n : } :
Vector α nVector α (n - 1)

The tail of a vector, with an empty vector having empty tail.

Equations
• One or more equations did not get rendered due to their size.
theorem Vector.tail_cons {α : Type u} {n : } (a : α) (v : Vector α n) :

The tail of a vector obtained by prepending is the vector prepended. to

@[simp]
theorem Vector.cons_head_tail {α : Type u} {n : } (v : Vector α ()) :
Vector.cons () () = v

Prepending the head of a vector to its tail gives the vector.

def Vector.toList {α : Type u} {n : } (v : Vector α n) :
List α

The list obtained from a vector.

Equations
• = v.val
def Vector.get {α : Type u} {n : } :
Vector α nFin nα

nth element of a vector, indexed by a Fin type.

Equations
• = match x, x with | { val := l, property := h }, i => List.nthLe l i (_ : i < )
def Vector.append {α : Type u} {n : } {m : } :
Vector α nVector α mVector α (n + m)

Appending a vector to another.

Equations
• = match x, x with | { val := l₁, property := h₁ }, { val := l₂, property := h₂ } => { val := l₁ ++ l₂, property := (_ : List.length (l₁ ++ l₂) = n + m) }
def Vector.elim {α : Type u_1} {C : {n : } → Vector α nSort u} (H : (l : List α) → C () { val := l, property := (_ : ) }) {n : } (v : Vector α n) :
C n v

Elimination rule for Vector.

Equations
• = match x with | { val := l, property := h } => match n, h with | .(), (_ : ) => H l
def Vector.map {α : Type u} {β : Type v} {n : } (f : αβ) :
Vector α nVector β n

Map a vector under a function.

Equations
@[simp]
theorem Vector.map_nil {α : Type u} {β : Type v} (f : αβ) :
Vector.map f Vector.nil = Vector.nil

A nil vector maps to a nil vector.

theorem Vector.map_cons {α : Type u} {β : Type v} {n : } (f : αβ) (a : α) (v : Vector α n) :
Vector.map f () = Vector.cons (f a) ()

map is natural with respect to cons.

def Vector.map₂ {α : Type u} {β : Type v} {φ : Type w} {n : } (f : αβφ) :
Vector α nVector β nVector φ n

Mapping two vectors under a curried function of two variables.

Equations
• One or more equations did not get rendered due to their size.
def Vector.replicate {α : Type u} (n : ) (a : α) :
Vector α n

Vector obtained by repeating an element.

Equations
• = { val := , property := (_ : = n) }
def Vector.drop {α : Type u} {n : } (i : ) :
Vector α nVector α (n - i)

Drop i elements from a vector of length n; we can have i > n.

Equations
• = match x with | { val := l, property := p } => { val := , property := (_ : List.length () = n - i) }
def Vector.take {α : Type u} {n : } (i : ) :
Vector α nVector α (min i n)

Take i elements from a vector of length n; we can have i > n.

Equations
• = match x with | { val := l, property := p } => { val := , property := (_ : List.length () = min i n) }
def Vector.removeNth {α : Type u} {n : } (i : Fin n) :
Vector α nVector α (n - 1)

Remove the element at position i from a vector of length n.

Equations
• = match x with | { val := l, property := p } => { val := , property := (_ : List.length () = n - 1) }
def Vector.ofFn {α : Type u} {n : } :
(Fin nα) → Vector α n

Vector of length n from a function on Fin n.

Equations
def Vector.mapAccumr {α : Type u} {β : Type v} {n : } {σ : Type} (f : ασσ × β) :
Vector α nσσ × Vector β n

Runs a function over a vector returning the intermediate results and a a final result.

Equations
• One or more equations did not get rendered due to their size.
def Vector.mapAccumr₂ {n : } {α : Type} {β : Type} {σ : Type} {φ : Type} (f : αβσσ × φ) :
Vector α nVector β nσσ × Vector φ n

Runs a function over a pair of vectors returning the intermediate results and a a final result.

Equations
• One or more equations did not get rendered due to their size.
theorem Vector.eq {α : Type u} {n : } (a1 : Vector α n) (a2 : Vector α n) :
a1 = a2

Vector is determined by the underlying list.

theorem Vector.eq_nil {α : Type u} (v : Vector α 0) :
v = Vector.nil

A vector of length 0 is a nil vector.

@[simp]
theorem Vector.toList_mk {α : Type u} {n : } (v : List α) (P : = n) :
Vector.toList { val := v, property := P } = v

Vector of length from a list v with witness that v has length n maps to v under toList.

@[simp]
theorem Vector.toList_nil {α : Type u} :
Vector.toList Vector.nil = []

A nil vector maps to a nil list.

@[simp]
theorem Vector.toList_length {α : Type u} {n : } (v : Vector α n) :

The length of the list to which a vector of length n maps is n.

@[simp]
theorem Vector.toList_cons {α : Type u} {n : } (a : α) (v : Vector α n) :

toList of cons of a vector and an element is the cons of the list obtained by toList and the element

@[simp]
theorem Vector.toList_append {α : Type u} {n : } {m : } (v : Vector α n) (w : Vector α m) :

Appending of vectors corresponds under toList to appending of lists.

@[simp]
theorem Vector.toList_drop {α : Type u} {n : } {m : } (v : Vector α m) :

drop of vectors corresponds under toList to drop of lists.

@[simp]
theorem Vector.toList_take {α : Type u} {n : } {m : } (v : Vector α m) :

take of vectors corresponds under toList to take of lists.