Vectors

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

structure Batteries.Vector (α : Type u) (n : Nat) extends Array α : Type u

Vector α n is an Array α with size n.

• toList : List α
• size_toArray : self.size = n

  Array size.

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

Equations

• Batteries.instReprVector = { reprPrec := Batteries.reprVector✝ }

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

Equations

• Batteries.instDecidableEqVector = Batteries.decEqVector✝

@[deprecated Batteries.Vector.size_toArray]

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

Alias of Batteries.Vector.size_toArray.

---

Array size.

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

Syntax for Vector α n

Equations

• One or more equations did not get rendered due to their size.

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

Custom eliminator for Vector α n through Array α

Equations

• Batteries.Vector.elimAsArray mk { toArray := a, size_toArray := ha } = mk a ha

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

Custom eliminator for Vector α n through List α

Equations

• Batteries.Vector.elimAsList mk { toList := a, size_toArray := ha } = mk a ha

@[inline]

def Batteries.Vector.empty {α : Type u_1} : Batteries.Vector α 0

The empty vector.

Equations

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

@[inline]

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

Make an empty vector with pre-allocated capacity.

Equations

• Batteries.Vector.mkEmpty capacity = { toArray := Array.mkEmpty capacity, size_toArray := ⋯ }

@[inline]

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

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

Equations

• Batteries.Vector.mkVector n v = { toArray := mkArray n v, size_toArray := ⋯ }

@[inline]

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

Returns a vector of size 1 with element v.

Equations

• Batteries.Vector.singleton v = { toArray := #[v], size_toArray := ⋯ }

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

Equations

• Batteries.Vector.instInhabited = { default := Batteries.Vector.mkVector n default }

@[inline]

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

Get an element of a vector using a Fin index.

Equations

• v.get i = v.get (Fin.cast ⋯ i)

@[inline]

def Batteries.Vector.uget {α : Type u_1} {n : Nat} (v : Batteries.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.

Equations

• v.uget i h = v.uget i ⋯

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

Equations

• Batteries.Vector.instGetElemNatLt = { getElem := fun (x : Batteries.Vector α n) (i : Nat) (h : i < n) => x.get ⟨i, h⟩ }

@[inline]

def Batteries.Vector.getD {α : Type u_1} {n : Nat} (v : Batteries.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.

Equations

• v.getD i default = v.getD i default

@[inline]

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

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

Equations

• v.back! = v.back!

@[inline]

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

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

Equations

• v.back? = v.back?

@[inline]

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

The last element of a non-empty vector.

Equations

• v.back = v.back!

@[inline]

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

The first element of a non-empty vector.

Equations

• v.head = v[0]

@[inline]

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

Push an element x to the end of a vector.

Equations

• Batteries.Vector.push x v = { toArray := v.push x, size_toArray := ⋯ }

@[inline]

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

Remove the last element of a vector.

Equations

• v.pop = { toArray := v.pop, size_toArray := ⋯ }

@[inline]

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

Set an element in a vector using a Fin index.

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

Equations

• v.set i x = { toArray := v.set (Fin.cast ⋯ i) x, size_toArray := ⋯ }

@[inline]

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

Set an element in a vector using a Nat index. By default, the get_elem_tactic is used to synthesize a proof that the index is within bounds.

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

Equations

• v.setN i x h = { toArray := v.setN i x ⋯, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.setD {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) : Batteries.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.

Equations

• v.setD i x = { toArray := v.setD i x, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.set! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) : Batteries.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.

Equations

• v.set! i x = { toArray := v.set! i x, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.append {α : Type u_1} {n m : Nat} (v : Batteries.Vector α n) (w : Batteries.Vector α m) : Batteries.Vector α (n + m)

Append two vectors.

Equations

• v.append w = { toArray := v.toArray ++ w.toArray, size_toArray := ⋯ }

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

Equations

• Batteries.Vector.instHAppendHAddNat = { hAppend := Batteries.Vector.append }

@[inline]

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

Creates a vector from another with a provably equal length.

Equations

• Batteries.Vector.cast h v = { toArray := v.toArray, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.extract {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (start stop : Nat) : Batteries.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.

Equations

• v.extract start stop = { toArray := v.extract start stop, size_toArray := ⋯ }

@[inline]

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

Maps elements of a vector using the function f.

Equations

• Batteries.Vector.map f v = { toArray := Array.map f v.toArray, size_toArray := ⋯ }

@[inline]

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

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

Equations

• a.zipWith b f = { toArray := a.zipWith b.toArray f, size_toArray := ⋯ }

@[inline]

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

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

Equations

• Batteries.Vector.ofFn f = { toArray := Array.ofFn f, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.swap {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i j : Fin n) : Batteries.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.

Equations

• v.swap i j = { toArray := v.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), size_toArray := ⋯ }

@[inline]

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

Swap two elements of a vector using Nat indices. By default, the get_elem_tactic is used to synthesize proofs that the indices are within bounds.

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

Equations

• v.swapN i j hi hj = { toArray := v.swapN i j ⋯ ⋯, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.swap! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i j : Nat) : Batteries.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.

Equations

• v.swap! i j = { toArray := v.swap! i j, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.swapAt {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) (x : α) : α × Batteries.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.

Equations

• v.swapAt i x = ((v.swapAt (Fin.cast ⋯ i) x).fst, { toArray := (v.swapAt (Fin.cast ⋯ i) x).snd, size_toArray := ⋯ })

@[inline]

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

Swaps an element of a vector with a given value using a Nat index. By default, the get_elem_tactic is used to synthesise a proof that the index is within 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.

Equations

• v.swapAtN i x h = ((v.swapAtN i x ⋯).fst, { toArray := (v.swapAtN i x ⋯).snd, size_toArray := ⋯ })

@[inline]

def Batteries.Vector.swapAt! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) : α × Batteries.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.

Equations

• v.swapAt! i x = ((v.swapAt! i x).fst, { toArray := (v.swapAt! i x).snd, size_toArray := ⋯ })

@[inline]

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

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

Equations

• Batteries.Vector.range n = { toArray := Array.range n, size_toArray := ⋯ }

@[inline]

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

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

• v.take m = { toArray := v.take m, size_toArray := ⋯ }

@[deprecated Batteries.Vector.take]

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

Alias of Batteries.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

• @Batteries.Vector.shrink = @Batteries.Vector.take

@[inline]

def Batteries.Vector.drop {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (m : Nat) : Batteries.Vector α (n - m)

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

Equations

• v.drop m = { toArray := v.extract m v.size, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.isEqv {α : Type u_1} {n : Nat} (v w : Batteries.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.

Equations

• v.isEqv w r = v.isEqvAux w.toArray ⋯ r 0 ⋯

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

Equations

• Batteries.Vector.instBEq = { beq := fun (a b : Batteries.Vector α n) => a.isEqv b fun (x1 x2 : α) => x1 == x2 }

@[inline]

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

Reverse the elements of a vector.

Equations

• v.reverse = { toArray := v.reverse, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.feraseIdx {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) : Batteries.Vector α (n - 1)

Delete an element of a vector using a Fin index.

Equations

• v.feraseIdx i = { toArray := v.feraseIdx (Fin.cast ⋯ i), size_toArray := ⋯ }

@[inline]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

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

Equations

• v.tail = if x : 0 < n then { toArray := v.eraseIdx 0, size_toArray := ⋯ } else Batteries.Vector.cast ⋯ v

@[inline]

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

Delete an element of a vector using a Nat index. By default, the get_elem_tactic is used to synthesise a proof that the index is within bounds.

Equations

• v.eraseIdxN i h = { toArray := v.eraseIdxN i ⋯, size_toArray := ⋯ }

@[inline]

def Batteries.Vector.indexOf? {α : Type u_1} {n : Nat} [BEq α] (v : Batteries.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.

Equations

• v.indexOf? x = match v.indexOf? x with | some res => some (Fin.cast ⋯ res) | none => none

@[inline]

def Batteries.Vector.isPrefixOf {α : Type u_1} {m n : Nat} [BEq α] (v : Batteries.Vector α m) (w : Batteries.Vector α n) : Bool

Returns true when v is a prefix of the vector w.

Equations

• v.isPrefixOf w = v.isPrefixOf w.toArray

@[inline]

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

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

Equations

• as.allDiff = as.allDiff