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.

source
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.

Equations

- List.Vector α n = { l : List α // l.length = n }

Instances For

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

- List.Vector.instDecidableEq = inferInstanceAs (DecidableEq { l : List α // l.length = n })

source
@[match_pattern]
def List.Vector.nil {α : Type u_1} :
Vector α 0

The empty vector with elements of type `α`

Equations

- List.Vector.nil = ⟨[], ⋯⟩

Instances For

source
@[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.

Equations

- List.Vector.cons x✝ ⟨v, h⟩ = ⟨x✝ :: v, ⋯⟩

Instances For

source
@[reducible]
def List.Vector.length {α : Type u_1} {n : ℕ} :
Vector α n → ℕ

The length of a vector.

Equations

- x✝.length = n

Instances For

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

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

Equations

- List.Vector.head ⟨a :: tail, property⟩ = a

Instances For

source
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.

source
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.

Equations

- List.Vector.tail ⟨[], h⟩ = ⟨[], ⋯⟩
- List.Vector.tail ⟨head :: v, h⟩ = ⟨v, ⋯⟩

Instances For

source
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

source
@[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.

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

The list obtained from a vector.

Equations

- v.toList = ↑v

Instances For

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

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

Equations

- l.get i = (↑l).get (Fin.cast ⋯ i)

Instances For

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

- List.Vector.instHAppendHAddNat = { hAppend := fun (x : List.Vector α n) (x_1 : List.Vector α m) => match x, x_1 with | ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, ⋯⟩ }

source
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₂, ⋯⟩
source
@[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.

Equations

- List.Vector.append ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ = ⟨l₁ ++ l₂, ⋯⟩

Instances For

source
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`.

Equations

- List.Vector.elim H ⟨l, ⋯⟩ = H l

Instances For

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

Map a vector under a function.

Equations

- List.Vector.map f ⟨l, h⟩ = ⟨List.map f l, ⋯⟩

Instances For

source
@[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.

source
@[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`.

source
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.

Equations

- List.Vector.pmap f ⟨l, h⟩ hp = ⟨List.pmap f l hp, ⋯⟩

Instances For

source
@[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
source
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.

Equations

- List.Vector.map₂ f ⟨x_2, property⟩ ⟨y, property_1⟩ = ⟨List.zipWith f x_2 y, ⋯⟩

Instances For

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

Vector obtained by repeating an element.

Equations

- List.Vector.replicate n a = ⟨List.replicate n a, ⋯⟩

Instances For

source
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`.

Equations

- List.Vector.drop i ⟨l, h⟩ = ⟨List.drop i l, ⋯⟩

Instances For

source
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`.

Equations

- List.Vector.take i ⟨l, h⟩ = ⟨List.take i l, ⋯⟩

Instances For

source
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`.

Equations

- List.Vector.eraseIdx i ⟨l, h⟩ = ⟨l.eraseIdx ↑i, ⋯⟩

Instances For

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

Vector of length `n` from a function on `Fin n`.

Equations

- List.Vector.ofFn x_2 = List.Vector.nil
- List.Vector.ofFn f = List.Vector.cons (f 0) (List.Vector.ofFn fun (i : Fin n) => f i.succ)

Instances For

source
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.

Equations

- List.Vector.congr h ⟨l, h_1⟩ = ⟨l, ⋯⟩

Instances For

source
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.

Equations

- List.Vector.mapAccumr f ⟨x_2, px⟩ x✝ = ((List.mapAccumr f x_2 x✝).fst, ⟨(List.mapAccumr f x_2 x✝).snd, ⋯⟩)

Instances For

source
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.

Equations

- List.Vector.mapAccumr₂ f ⟨x_3, px⟩ ⟨y, py⟩ x✝ = ((List.mapAccumr₂ f x_3 y x✝).fst, ⟨(List.mapAccumr₂ f x_3 y x✝).snd, ⋯⟩)

Instances For

### Shift Primitives #

source
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`.

Equations

- v.shiftLeftFill i fill = List.Vector.congr ⋯ (List.Vector.drop i v ++ List.Vector.replicate (min n i) fill)

Instances For

source
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`.

Equations

- v.shiftRightFill i fill = List.Vector.congr ⋯ (List.Vector.replicate (min n i) fill ++ List.Vector.take (n - i) v)

Instances For

### Basic Theorems #

source
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.

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

A vector of length `0` is a `nil` vector.

source
@[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`.

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

A nil vector maps to a nil list.

source
@[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`.

source
@[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

source
@[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.

source
@[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.

source
@[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.

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

- List.Vector.instGetElemNatLt = { getElem := fun (x : List.Vector α n) (i : ℕ) (h : i < n) => x.get ⟨i, h⟩ }

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