Vectors

Vector α n is a thin wrapper around Array α for arrays of fixed size n.

structure Vector (α : Type u) (n : Nat) : Type u

Vector α n is an Array α with size n.

• toArray : Array α

  The underlying array.

• size_toArray : self.toArray.size = n

  Array size.

instance instReprVector {α✝ : Type u_1} {n✝ : Nat} [Repr α✝] : Repr (Vector α✝ n✝)

instance instDecidableEqVector {α✝ : Type u_1} {n✝ : Nat} [DecidableEq α✝] : DecidableEq (Vector α✝ n✝)

@[reducible, inline]

abbrev Array.toVector {α : Type u_1} (xs : Array α) : Vector α xs.size

Converts an array to a vector. The resulting vector's size is the array's size.

@[reducible, inline]

abbrev Vector.size {α : Type u_1} {n : Nat} : Vector α n → Nat

The size of a vector.

def Vector.«term#v[_,]» : Lean.ParserDescr

Syntax for Vector α n

Conventions for notations in identifiers:

• The recommended spelling of #v[] in identifiers is empty.

• The recommended spelling of #v[x] in identifiers is singleton.

def Vector.toList {α : Type u_1} {n : Nat} (xs : Vector α n) : List α

Convert a vector to a list.

def Vector.elimAsArray {α : Type u_1} {n : Nat} {motive : Vector α n → Sort u} (mk : (xs : Array α) → (ha : xs.size = n) → motive { toArray := xs, size_toArray := ha }) (xs : Vector α n) : motive xs

Custom eliminator for Vector α n through Array α

def Vector.elimAsList {α : Type u_1} {n : Nat} {motive : Vector α n → Sort u} (mk : (l : List α) → (ha : l.length = n) → motive { toArray := { toList := l }, size_toArray := ha }) (xs : Vector α n) : motive xs

Custom eliminator for Vector α n through List α

@[inline]

def Vector.emptyWithCapacity {α : Type u_1} (capacity : Nat) : Vector α 0

Make an empty vector with pre-allocated capacity.

@[reducible, inline, deprecated Vector.emptyWithCapacity (since := "2025-03-12")]

abbrev Vector.mkEmpty {α : Type u_1} (capacity : Nat) : Vector α 0

Make an empty vector with pre-allocated capacity.

@[inline]

def Vector.replicate {α : Type u_1} (n : Nat) (v : α) : Vector α n

Makes a vector of size n with all cells containing v.

@[reducible, inline, deprecated Vector.replicate (since := "2025-03-18")]

abbrev Vector.mkVector {α : Type u_1} (n : Nat) (v : α) : Vector α n

instance Vector.instNonemptyOfNatNat {α : Type u_1} : Nonempty (Vector α 0)

instance Vector.instNonempty {α : Type u_1} {n : Nat} [Nonempty α] : Nonempty (Vector α n)

@[inline]

def Vector.singleton {α : Type u_1} (v : α) : Vector α 1

Returns a vector of size 1 with element v.

instance Vector.instInhabited {α : Type u_1} {n : Nat} [Inhabited α] : Inhabited (Vector α n)

@[inline]

def Vector.get {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Fin n) : α

Get an element of a vector using a Fin index.

@[inline]

def Vector.uget {α : Type u_1} {n : Nat} (xs : Vector α n) (i : USize) (h : i.toNat < n) : α

Get an element of a vector using a USize index and a proof that the index is within bounds.

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

def Vector.contains {α : Type u_1} {n : Nat} [BEq α] (xs : Vector α n) (a : α) : Bool

Check if there is an element which satisfies a == ·.

structure Vector.Mem {α : Type u_1} {n : Nat} (xs : Vector α n) (a : α) : Prop

a ∈ v is a predicate which asserts that a is in the vector v.

• val : a ∈ xs.toArray

instance Vector.instMembership {α : Type u_1} {n : Nat} : Membership α (Vector α n)

@[inline]

def Vector.getD {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (default : α) : α

Get an element of a vector using a Nat index. Returns the given default value if the index is out of bounds.

@[inline]

def Vector.back! {α : Type u_1} {n : Nat} [Inhabited α] (xs : Vector α n) : α

The last element of a vector. Panics if the vector is empty.

@[inline]

def Vector.back? {α : Type u_1} {n : Nat} (xs : Vector α n) : Option α

The last element of a vector, or none if the vector is empty.

@[inline]

def Vector.back {n : Nat} {α : Type u_1} [NeZero n] (xs : Vector α n) : α

The last element of a non-empty vector.

@[inline]

def Vector.head {n : Nat} {α : Type u_1} [NeZero n] (xs : Vector α n) : α

The first element of a non-empty vector.

@[inline]

def Vector.push {α : Type u_1} {n : Nat} (xs : Vector α n) (x : α) : Vector α (n + 1)

Push an element x to the end of a vector.

@[inline]

def Vector.pop {α : Type u_1} {n : Nat} (xs : Vector α n) : Vector α (n - 1)

Remove the last element of a vector.

@[inline]

def Vector.set {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (x : α) (h : i < n := by get_elem_tactic) : Vector α n

Set an element in a vector using a Nat index, with a tactic provided proof that the index is in bounds.

This will perform the update destructively provided that the vector has a reference count of 1.

@[inline]

def Vector.setIfInBounds {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (x : α) : Vector α n

Set an element in a vector using a Nat index. Returns the vector unchanged if the index is out of bounds.

This will perform the update destructively provided that the vector has a reference count of 1.

@[inline]

def Vector.set! {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (x : α) : Vector α n

Set an element in a vector using a Nat index. Panics if the index is out of bounds.

This will perform the update destructively provided that the vector has a reference count of 1.

@[inline]

def Vector.foldlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} [Monad m] (f : β → α → m β) (b : β) (xs : Vector α n) : m β

@[inline]

def Vector.foldrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] (f : α → β → m β) (b : β) (xs : Vector α n) : m β

@[inline]

def Vector.foldl {β : Type u_1} {α : Type u_2} {n : Nat} (f : β → α → β) (b : β) (xs : Vector α n) : β

@[inline]

def Vector.foldr {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → β → β) (b : β) (xs : Vector α n) : β

@[inline]

def Vector.append {α : Type u_1} {n m : Nat} (xs : Vector α n) (ys : Vector α m) : Vector α (n + m)

Append two vectors.

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

@[inline]

def Vector.cast {n m : Nat} {α : Type u_1} (h : n = m) (xs : Vector α n) : Vector α m

Creates a vector from another with a provably equal length.

@[inline]

def Vector.extract {α : Type u_1} {n : Nat} (xs : Vector α n) (start : Nat := 0) (stop : Nat := n) : Vector α (min stop n - start)

Extracts the slice of a vector from indices start to stop (exclusive). If start ≥ stop, the result is empty. If stop is greater than the size of the vector, the size is used instead.

@[inline]

def Vector.take {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) : Vector α (min i n)

Extract the first i elements of a vector. If i is greater than or equal to the size of the vector then the vector is returned unchanged.

We immediately simplify this to the extract operation, so there is no verification API for this function.

@[simp]

theorem Vector.take_eq_extract {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) : xs.take i = xs.extract 0 i

@[inline]

def Vector.drop {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) : Vector α (n - i)

Deletes the first i elements of a vector. If i is greater than or equal to the size of the vector then the empty vector is returned.

We immediately simplify this to the extract operation, so there is no verification API for this function.

@[simp]

theorem Vector.drop_eq_cast_extract {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) : xs.drop i = Vector.cast ⋯ (xs.extract i)

@[inline]

def Vector.shrink {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) : Vector α (min i n)

Shrinks a vector to the first m elements, by repeatedly popping the last element.

We immediately simplify this to the extract operation, so there is no verification API for this function.

@[simp]

theorem Vector.shrink_eq_take {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) : xs.shrink i = xs.take i

@[inline]

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

Maps elements of a vector using the function f.

@[inline]

def Vector.mapIdx {α : Type u_1} {β : Type u_2} {n : Nat} (f : Nat → α → β) (xs : Vector α n) : Vector β n

Maps elements of a vector using the function f, which also receives the index of the element.

@[inline]

def Vector.mapFinIdx {α : Type u_1} {n : Nat} {β : Type u_2} (xs : Vector α n) (f : (i : Nat) → α → i < n → β) : Vector β n

Maps elements of a vector using the function f, which also receives the index of the element, and the fact that the index is less than the size of the vector.

@[inline]

def Vector.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] (f : α → m β) (xs : Vector α n) : m (Vector β n)

Map a monadic function over a vector.

@[irreducible]

def Vector.mapM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] (f : α → m β) (xs : Vector α n) (k : Nat) (h : k ≤ n) (acc : Vector β k) : m (Vector β n)

@[inline]

def Vector.forM {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} [Monad m] (xs : Vector α n) (f : α → m PUnit) : m PUnit

@[inline]

def Vector.flatMapM {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} {k : Nat} [Monad m] (xs : Vector α n) (f : α → m (Vector β k)) : m (Vector β (n * k))

@[irreducible]

def Vector.flatMapM.go {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} {k : Nat} [Monad m] (xs : Vector α n) (f : α → m (Vector β k)) (i : Nat) (h : i ≤ n) (acc : Vector β (i * k)) : m (Vector β (n * k))

@[inline]

def Vector.mapFinIdxM {n : Nat} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (xs : Vector α n) (f : (i : Nat) → α → i < n → m β) : m (Vector β n)

Variant of mapIdxM which receives the index i along with the bound `i < n.

@[specialize #[]]

def Vector.mapFinIdxM.map {n : Nat} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (xs : Vector α n) (f : (i : Nat) → α → i < n → m β) (i j : Nat) (inv : i + j = n) (ys : Vector β (n - i)) : m (Vector β n)

@[inline]

def Vector.mapIdxM {n : Nat} {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (xs : Vector α n) : m (Vector β n)

@[inline]

def Vector.firstM {β : Type v} {n : Nat} {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (xs : Vector α n) : m β

@[inline]

def Vector.flatten {α : Type u_1} {n m : Nat} (xs : Vector (Vector α n) m) : Vector α (m * n)

@[inline]

def Vector.flatMap {α : Type u_1} {n : Nat} {β : Type u_2} {m : Nat} (xs : Vector α n) (f : α → Vector β m) : Vector β (n * m)

@[inline]

def Vector.zipIdx {α : Type u_1} {n : Nat} (xs : Vector α n) (k : Nat := 0) : Vector (α × Nat) n

@[reducible, inline, deprecated Vector.zipIdx (since := "2025-01-21")]

abbrev Vector.zipWithIndex {α : Type u_1} {n : Nat} (xs : Vector α n) (k : Nat := 0) : Vector (α × Nat) n

@[inline]

def Vector.zip {α : Type u_1} {n : Nat} {β : Type u_2} (as : Vector α n) (bs : Vector β n) : Vector (α × β) n

@[inline]

def Vector.zipWith {α : Type u_1} {β : Type u_2} {φ : Type u_3} {n : Nat} (f : α → β → φ) (as : Vector α n) (bs : Vector β n) : Vector φ n

Maps corresponding elements of two vectors of equal size using the function f.

@[inline]

def Vector.unzip {α : Type u_1} {β : Type u_2} {n : Nat} (xs : Vector (α × β) n) : Vector α n × Vector β n

@[inline]

def Vector.ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : Vector α n

The vector of length n whose i-th element is f i.

See also Vector.ofFnM defined in Init.Data.Vector.OfFn.

@[inline]

def Vector.swap {α : Type u_1} {n : Nat} (xs : Vector α n) (i j : Nat) (hi : i < n := by get_elem_tactic) (hj : j < n := by get_elem_tactic) : Vector α n

Swap two elements of a vector using Fin indices.

This will perform the update destructively provided that the vector has a reference count of 1.

@[inline]

def Vector.swapIfInBounds {α : Type u_1} {n : Nat} (xs : Vector α n) (i j : Nat) : Vector α n

Swap two elements of a vector using Nat indices. Panics if either index is out of bounds.

This will perform the update destructively provided that the vector has a reference count of 1.

@[inline]

def Vector.swapAt {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (x : α) (hi : i < n := by get_elem_tactic) : α × Vector α n

Swaps an element of a vector with a given value using a Fin index. The original value is returned along with the updated vector.

This will perform the update destructively provided that the vector has a reference count of 1.

@[inline]

def Vector.swapAt! {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (x : α) : α × Vector α n

Swaps an element of a vector with a given value using a Nat index. Panics if the index is out of bounds. The original value is returned along with the updated vector.

This will perform the update destructively provided that the vector has a reference count of 1.

@[inline]

def Vector.range (n : Nat) : Vector Nat n

The vector #v[0, 1, 2, ..., n-1].

@[inline]

def Vector.range' (start size : Nat) (step : Nat := 1) : Vector Nat size

The vector #v[start, start + step, start + 2 * step, ..., start + (size - 1) * step].

@[inline]

def Vector.isEqv {α : Type u_1} {n : Nat} (xs ys : Vector α n) (r : α → α → Bool) : Bool

Compares two vectors of the same size using a given boolean relation r. isEqv v w r returns true if and only if r v[i] w[i] is true for all indices i.

instance Vector.instBEq {α : Type u_1} {n : Nat} [BEq α] : BEq (Vector α n)

@[inline]

def Vector.reverse {α : Type u_1} {n : Nat} (xs : Vector α n) : Vector α n

Reverse the elements of a vector.

@[inline]

def Vector.eraseIdx {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) : Vector α (n - 1)

Delete an element of a vector using a Nat index and a tactic provided proof.

@[inline]

def Vector.eraseIdx! {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) : Vector α (n - 1)

Delete an element of a vector using a Nat index. Panics if the index is out of bounds.

@[inline]

def Vector.insertIdx {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (x : α) (h : i ≤ n := by get_elem_tactic) : Vector α (n + 1)

Insert an element into a vector using a Nat index and a tactic provided proof.

@[inline]

def Vector.insertIdx! {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (x : α) : Vector α (n + 1)

Insert an element into a vector using a Nat index. Panics if the index is out of bounds.

@[inline]

def Vector.tail {α : Type u_1} {n : Nat} (xs : Vector α n) : Vector α (n - 1)

Delete the first element of a vector. Returns the empty vector if the input vector is empty.

We immediately simplify this to the extract operation, so there is no verification API for this function.

@[simp]

theorem Vector.tail_eq_cast_extract {α : Type u_1} {n : Nat} (xs : Vector α n) : xs.tail = Vector.cast ⋯ (xs.extract 1)

@[inline]

def Vector.finIdxOf? {α : Type u_1} {n : Nat} [BEq α] (xs : Vector α n) (x : α) : Option (Fin n)

Finds the first index of a given value in a vector using == for comparison. Returns none if the no element of the index matches the given value.

@[reducible, inline, deprecated Vector.finIdxOf? (since := "2025-01-29")]

abbrev Vector.indexOf? {α : Type u_1} {n : Nat} [BEq α] (xs : Vector α n) (x : α) : Option (Fin n)

@[inline]

def Vector.findFinIdx? {α : Type u_1} {n : Nat} (p : α → Bool) (xs : Vector α n) : Option (Fin n)

Finds the first index of a given value in a vector using a predicate. Returns none if the no element of the index matches the given value.

@[inline]

def Vector.findM? {n : Nat} {α : Type} {m : Type → Type} [Monad m] (f : α → m Bool) (as : Vector α n) : m (Option α)

Note that the universe level is constrained to Type here, to avoid having to have the predicate live in p : α → m (ULift Bool).

@[inline]

def Vector.findSomeM? {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] (f : α → m (Option β)) (as : Vector α n) : m (Option β)

@[inline]

def Vector.findRevM? {n : Nat} {α : Type} {m : Type → Type} [Monad m] (f : α → m Bool) (as : Vector α n) : m (Option α)

Note that the universe level is constrained to Type here, to avoid having to have the predicate live in p : α → m (ULift Bool).

@[inline]

def Vector.findSomeRevM? {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] (f : α → m (Option β)) (as : Vector α n) : m (Option β)

@[inline]

def Vector.find? {n : Nat} {α : Type} (f : α → Bool) (as : Vector α n) : Option α

@[inline]

def Vector.findRev? {n : Nat} {α : Type} (f : α → Bool) (as : Vector α n) : Option α

@[inline]

def Vector.findSome? {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → Option β) (as : Vector α n) : Option β

@[inline]

def Vector.findSomeRev? {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → Option β) (as : Vector α n) : Option β

@[inline]

def Vector.isPrefixOf {α : Type u_1} {m n : Nat} [BEq α] (xs : Vector α m) (ys : Vector α n) : Bool

Returns true when xs is a prefix of the vector ys.

@[inline]

def Vector.anyM {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] (p : α → m Bool) (xs : Vector α n) : m Bool

Returns true with the monad if p returns true for any element of the vector.

@[inline]

def Vector.allM {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] (p : α → m Bool) (xs : Vector α n) : m Bool

Returns true with the monad if p returns true for all elements of the vector.

@[inline]

def Vector.any {α : Type u_1} {n : Nat} (xs : Vector α n) (p : α → Bool) : Bool

Returns true if p returns true for any element of the vector.

@[inline]

def Vector.all {α : Type u_1} {n : Nat} (xs : Vector α n) (p : α → Bool) : Bool

Returns true if p returns true for all elements of the vector.

@[inline]

def Vector.countP {α : Type u_1} {n : Nat} (p : α → Bool) (xs : Vector α n) : Nat

Count the number of elements of a vector that satisfy the predicate p.

@[inline]

def Vector.count {α : Type u_1} {n : Nat} [BEq α] (a : α) (xs : Vector α n) : Nat

Count the number of elements of a vector that are equal to a.

@[inline]

def Vector.replace {α : Type u_1} {n : Nat} [BEq α] (xs : Vector α n) (a b : α) : Vector α n

@[inline]

def Vector.sum {α : Type u_1} {n : Nat} [Add α] [Zero α] (xs : Vector α n) : α

Computes the sum of the elements of a vector.

Examples:

• #v[a, b, c].sum = a + (b + (c + 0))
• #v[1, 2, 5].sum = 8

@[inline]

def Vector.leftpad {α : Type u_1} {m : Nat} (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m)

Pad a vector on the left with a given element.

Note that we immediately simplify this to an ++ operation, and do not provide separate verification theorems.

@[inline]

def Vector.rightpad {α : Type u_1} {m : Nat} (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m)

Pad a vector on the right with a given element.

Note that we immediately simplify this to an ++ operation, and do not provide separate verification theorems.

ForIn instance

@[simp]

theorem Vector.mem_toArray_iff {α : Type u_1} {n : Nat} (a : α) (xs : Vector α n) : a ∈ xs.toArray ↔ a ∈ xs

instance Vector.instForIn'InferInstanceMembership {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} : ForIn' m (Vector α n) α inferInstance

ForM instance

instance Vector.instForM {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} : ForM m (Vector α n) α

@[simp]

theorem Vector.forM_eq_forM {m : Type u_1 → Type u_2} {α : Type u_3} {n✝ : Nat} {v : Vector α n✝} [Monad m] (f : α → m PUnit) : v.forM f = forM v f

ToStream instance

instance Vector.instToStreamSubarray {α : Type u_1} {n : Nat} : ToStream (Vector α n) (Subarray α)

Lexicographic ordering

instance Vector.instLT {α : Type u_1} {n : Nat} [LT α] : LT (Vector α n)

instance Vector.instLE {α : Type u_1} {n : Nat} [LT α] : LE (Vector α n)

def Vector.lex {α : Type u_1} {n : Nat} [BEq α] (xs ys : Vector α n) (lt : α → α → Bool := by exact (· < ·)) : Bool

Lexicographic comparator for vectors.

lex v w lt is true if

• v is pairwise equivalent via == to w, or
• there is an index i such that lt v[i] w[i], and for all j < i, v[j] == w[j].