Vectors

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

structure 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 instReprVector {α✝ : Type u_1} {n✝ : Nat} [Repr α✝] : Repr (Vector α✝ n✝)

Equations

• instReprVector = { reprPrec := reprVector✝ }

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

Equations

• instDecidableEqVector = decEqVector✝

@[reducible, inline]

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

Convert xs : Array α to Vector α xs.size.

Equations

• xs.toVector = { toArray := xs, size_toArray := ⋯ }

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

Syntax for Vector α n

Equations

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

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

Custom eliminator for Vector α n through Array α

Equations

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

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

Custom eliminator for Vector α n through List α

Equations

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

@[inline]

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

Make an empty vector with pre-allocated capacity.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

Returns a vector of size 1 with element v.

Equations

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

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

Equations

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

@[inline]

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

Get an element of a vector using a Fin index.

Equations

• v.get i = v.toArray[↑(Fin.cast ⋯ i)]

@[inline]

def Vector.uget {α : Type u_1} {n : Nat} (v : 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 Vector.instGetElemNatLt {α : Type u_1} {n : Nat} : GetElem (Vector α n) Nat α fun (x : Vector α n) (i : Nat) => i < n

Equations

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

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

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

Equations

• v.contains a = v.contains a

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

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

• val : a ∈ as.toArray

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

Equations

• Vector.instMembership = { mem := Vector.Mem }

@[inline]

def Vector.getD {α : Type u_1} {n : Nat} (v : 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 Vector.back! {α : Type u_1} {n : Nat} [Inhabited α] (v : Vector α n) : α

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

Equations

• v.back! = v.back!

@[inline]

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

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

Equations

• v.back? = v.back?

@[inline]

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

The last element of a non-empty vector.

Equations

• v.back = v.back!

@[inline]

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

The first element of a non-empty vector.

Equations

• v.head = v[0]

@[inline]

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

Push an element x to the end of a vector.

Equations

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

@[inline]

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

Remove the last element of a vector.

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Append two vectors.

Equations

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

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

Equations

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

@[inline]

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

Creates a vector from another with a provably equal length.

Equations

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

@[inline]

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

Maps elements of a vector using the function f.

Equations

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

@[inline]

def Vector.zipWith {α : Type u_1} {n : Nat} {β : Type u_2} {φ : Type u_3} (a : Vector α n) (b : Vector β n) (f : α → β → φ) : 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 Vector.ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : Vector α n

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

Equations

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

@[inline]

def Vector.swap {α : 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

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 hi hj = { toArray := v.swap i j ⋯ ⋯, size_toArray := ⋯ }

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

def Vector.take {α : Type u_1} {n : Nat} (v : Vector α n) (m : Nat) : 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 := ⋯ }

@[inline]

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

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

Equations

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

@[inline]

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

Reverse the elements of a vector.

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• v.eraseIdx! i = if x : i < n then v.eraseIdx i x else let_fun this := { default := v.pop }; panicWithPosWithDecl "Init.Data.Vector.Basic" "Vector.eraseIdx!" 249 4 "index out of bounds"

@[inline]

def Vector.tail {α : Type u_1} {n : Nat} (v : Vector α n) : 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 v.eraseIdx 0 x else Vector.cast ⋯ v

@[inline]

def Vector.indexOf? {α : Type u_1} {n : Nat} [BEq α] (v : 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 = Option.map (Fin.cast ⋯) (v.indexOf? x)

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• Vector.anyM p v = Array.anyM p v.toArray

@[inline]

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

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

Equations

• Vector.allM p v = Array.allM p v.toArray

@[inline]

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

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

Equations

• v.any p = v.any p

@[inline]

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

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

Equations

• v.all p = v.all p

Lexicographic ordering

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

Equations

• Vector.instLT = { lt := fun (v w : Vector α n) => v.toArray < w.toArray }

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

Equations

• Vector.instLE = { le := fun (v w : Vector α n) => v.toArray ≤ w.toArray }

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

Equations

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