Vectors

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

@[deprecated Vector.size_toArray]

theorem Vector.size_eq {α : Type u} {n : Nat} (self : Vector α n) : self.size = n

Alias of Vector.size_toArray.

---

Array size.

@[deprecated Vector.set]

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

Alias of Vector.set.

---

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.

Equations

• @Vector.setN = @Vector.set

@[deprecated Vector.setIfInBounds]

def Vector.setD {α : Type u_1} {n : Nat} (v : Vector α n) (i : Nat) (x : α) : Vector α n

Alias of Vector.setIfInBounds.

---

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.

Equations

• @Vector.setD = @Vector.setIfInBounds

@[deprecated Vector.swap]

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

Alias of Vector.swap.

---

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.

Equations

• @Vector.swapN = @Vector.swap

@[deprecated Vector.swapIfInBounds]

def Vector.swap! {α : Type u_1} {n : Nat} (v : Vector α n) (i j : Nat) : Vector α n

Alias of Vector.swapIfInBounds.

---

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.

Equations

• @Vector.swap! = @Vector.swapIfInBounds

@[deprecated Vector.swapAt]

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

Alias of Vector.swapAt.

---

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.

Equations

• @Vector.swapAtN = @Vector.swapAt

@[deprecated Vector.take]

def Vector.shrink {α : Type u_1} {n : Nat} (v : Vector α n) (m : Nat) : Vector α (min m n)

Alias of Vector.take.

---

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

Equations

• @Vector.shrink = @Vector.take

@[deprecated Vector.eraseIdx]

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

Alias of Vector.eraseIdx.

---

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

Equations

• @Vector.eraseIdxN = @Vector.eraseIdx

@[deprecated]

def Vector.empty (α : Type u) : Vector α 0

Use #v[] instead.

Equations

• Vector.empty α = { toArray := #[], size_toArray := ⋯ }

@[inline]

def Vector.allDiff {α : Type u_1} {n : Nat} [BEq α] (as : Vector α n) : Bool

Returns true when all elements of the vector are pairwise distinct using == for comparison.

Equations

• as.allDiff = as.allDiff