The type List.Vector represents lists with fixed length.

TODO: The API of List.Vector is quite incomplete relative to Vector, and in particular does not use x[i] (that is GetElem notation) as the preferred accessor. Any combination of reducing the use of List.Vector in Mathlib, or modernising its API, would be welcome.

def List.Vector (α : Type u) (n : ℕ) : Type u

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

Note that there is also Vector α n in the root namespace, which is the type of arrays of length n with elements of type α.

Typically, if you are doing programming or verification, you will primarily use Vector α n, and if you are doing mathematics, you may want to use List.Vector α n instead.

instance List.Vector.instDecidableEq {α : Type u_1} {n : ℕ} [DecidableEq α] : DecidableEq (Vector α n)

@[match_pattern]

def List.Vector.nil {α : Type u_1} : Vector α 0

The empty vector with elements of type α

@[match_pattern]

def List.Vector.cons {α : Type u_1} {n : ℕ} : α → Vector α n → Vector α n.succ

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.

@[reducible]

def List.Vector.length {α : Type u_1} {n : ℕ} : Vector α n → ℕ

The length of a vector.

def List.Vector.head {α : Type u_1} {n : ℕ} : Vector α n.succ → α

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

theorem List.Vector.head_cons {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) : (cons a v).head = a

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

def List.Vector.tail {α : Type u_1} {n : ℕ} : Vector α n → Vector α (n - 1)

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

theorem List.Vector.tail_cons {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) : (cons a v).tail = v

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

@[simp]

theorem List.Vector.cons_head_tail {α : Type u_1} {n : ℕ} (v : Vector α n.succ) : cons v.head v.tail = v

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

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

The list obtained from a vector.

def List.Vector.get {α : Type u_1} {n : ℕ} (l : Vector α n) (i : Fin n) : α

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

instance List.Vector.instHAppendHAddNat {α : Type u_1} {n m : ℕ} : HAppend (Vector α n) (Vector α m) (Vector α (n + m))

theorem List.Vector.append_def {α : Type u_1} {n m : ℕ} : HAppend.hAppend = fun (x : Vector α n) (x_1 : Vector α m) => match x, x_1 with | ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, ⋯⟩

@[deprecated "use `++` instead" (since := "2025-06-05")]

def List.Vector.append {α : Type u_1} {n m : ℕ} : Vector α n → Vector α m → Vector α (n + m)

Appending a vector to another.

def List.Vector.elim {α : Type u_5} {C : {n : ℕ} → Vector α n → Sort u} (H : (l : List α) → C ⟨l, ⋯⟩) {n : ℕ} (v : Vector α n) : C v

Elimination rule for Vector.

def List.Vector.map {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) : Vector α n → Vector β n

Map a vector under a function.

@[simp]

theorem List.Vector.map_nil {α : Type u_1} {β : Type u_2} (f : α → β) : map f nil = nil

A nil vector maps to a nil vector.

@[simp]

theorem List.Vector.map_cons {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (a : α) (v : Vector α n) : map f (cons a v) = cons (f a) (map f v)

map is natural with respect to cons.

def List.Vector.pmap {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n) : (∀ (x : α), x ∈ v.toList → p x) → Vector β n

Map a vector under a partial function.

@[simp]

theorem List.Vector.pmap_nil {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (hp : ∀ (x : α), x ∈ nil.toList → p x) : pmap f nil hp = nil

def List.Vector.map₂ {α : Type u_1} {β : Type u_2} {φ : Type u_4} {n : ℕ} (f : α → β → φ) : Vector α n → Vector β n → Vector φ n

Mapping two vectors under a curried function of two variables.

def List.Vector.replicate {α : Type u_1} (n : ℕ) (a : α) : Vector α n

Vector obtained by repeating an element.

def List.Vector.drop {α : Type u_1} {n : ℕ} (i : ℕ) : Vector α n → Vector α (n - i)

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

def List.Vector.take {α : Type u_1} {n : ℕ} (i : ℕ) : Vector α n → Vector α (min i n)

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

def List.Vector.eraseIdx {α : Type u_1} {n : ℕ} (i : Fin n) : Vector α n → Vector α (n - 1)

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

def List.Vector.ofFn {α : Type u_1} {n : ℕ} : (Fin n → α) → Vector α n

Vector of length n from a function on Fin n.

def List.Vector.congr {α : Type u_1} {n m : ℕ} (h : n = m) : Vector α n → Vector α m

Create a vector from another with a provably equal length.

def List.Vector.mapAccumr {α : Type u_1} {β : Type u_2} {σ : Type u_3} {n : ℕ} (f : α → σ → σ × β) : Vector α n → σ → σ × Vector β n

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

def List.Vector.mapAccumr₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {φ : Type u_4} {n : ℕ} (f : α → β → σ → σ × φ) : Vector α n → Vector β n → σ → σ × Vector φ n

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

Shift Primitives

def List.Vector.shiftLeftFill {α : Type u_1} {n : ℕ} (v : Vector α n) (i : ℕ) (fill : α) : Vector α n

shiftLeftFill v i is the vector obtained by left-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

def List.Vector.shiftRightFill {α : Type u_1} {n : ℕ} (v : Vector α n) (i : ℕ) (fill : α) : Vector α n

shiftRightFill v i is the vector obtained by right-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

Basic Theorems

theorem List.Vector.eq {α : Type u_1} {n : ℕ} (a1 a2 : Vector α n) : a1.toList = a2.toList → a1 = a2

Vector is determined by the underlying list.

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

A vector of length 0 is a nil vector.

@[simp]

theorem List.Vector.toList_mk {α : Type u_1} {n : ℕ} (v : List α) (P : v.length = n) : toList ⟨v, P⟩ = v

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

@[simp]

theorem List.Vector.toList_nil {α : Type u_1} : nil.toList = []

A nil vector maps to a nil list.

@[simp]

theorem List.Vector.toList_length {α : Type u_1} {n : ℕ} (v : Vector α n) : v.toList.length = n

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

@[simp]

theorem List.Vector.toList_cons {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) : (cons a v).toList = a :: v.toList

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

@[simp]

theorem List.Vector.toList_append {α : Type u_1} {n m : ℕ} (v : Vector α n) (w : Vector α m) : (v ++ w).toList = v.toList ++ w.toList

Appending of vectors corresponds under toList to appending of lists.

@[simp]

theorem List.Vector.toList_drop {α : Type u_1} {n m : ℕ} (v : Vector α m) : (drop n v).toList = List.drop n v.toList

drop of vectors corresponds under toList to drop of lists.

@[simp]

theorem List.Vector.toList_take {α : Type u_1} {n m : ℕ} (v : Vector α m) : (take n v).toList = List.take n v.toList

take of vectors corresponds under toList to take of lists.

instance List.Vector.instGetElemNatLt {α : Type u_1} {n : ℕ} : GetElem (Vector α n) ℕ α fun (x : Vector α n) (i : ℕ) => i < n

theorem List.Vector.getElem_def {α : Type u_1} {n : ℕ} (v : Vector α n) (i : ℕ) {hi : i < n} : v[i] = v.toList[i]

theorem List.Vector.toList_getElem {α : Type u_1} {n : ℕ} (v : Vector α n) (i : ℕ) {hi : i < v.toList.length} : v.toList[i] = v[i]