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.

Instances For

• Vector.instBEq
• Vector.instForIn'InferInstanceMembership
• Vector.instForM
• Vector.instGetElemNatLt
• Vector.instHAppendHAddNat
• Vector.instInhabited
• Vector.instLE
• Vector.instLT
• Vector.instLawfulBEq
• Vector.instMembership
• Vector.instNonempty
• Vector.instNonemptyOfNatNat
• Vector.instToStreamSubarray
• instReprVector

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

Conventions for notations in identifiers:

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

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

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 : (xs : Array α) → (ha : xs.size = n) → motive { toArray := xs, size_toArray := ha }) (xs : Vector α n) : motive xs

Custom eliminator for Vector α n through Array α

Equations

• Vector.elimAsArray mk { toArray := xs, size_toArray := h } = mk xs h

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

Custom eliminator for Vector α n through List α

Equations

• Vector.elimAsList mk { toList := xs, size_toArray := ha } = mk xs 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 := ⋯ }

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.

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} (xs : Vector α n) (i : Fin n) : α

Get an element of a vector using a Fin index.

Equations

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

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

Equations

• xs.uget i h = xs.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 (xs : Vector α n) (i : Nat) (h : i < n) => xs.get ⟨i, h⟩ }

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

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

Equations

• xs.contains a = xs.contains 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)

Equations

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

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

Equations

• xs.getD i default = xs.getD i default

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

Equations

• xs.back! = xs.back!

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

Equations

• xs.back? = xs.back?

@[inline]

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

The last element of a non-empty vector.

Equations

• xs.back = xs[n - 1]

@[inline]

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

The first element of a non-empty vector.

Equations

• xs.head = xs[0]

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

Equations

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

@[inline]

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

Remove the last element of a vector.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Vector.foldlM f b xs = Array.foldlM f b xs.toArray

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

Equations

• Vector.foldrM f b xs = Array.foldrM f b xs.toArray

@[inline]

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

Equations

• Vector.foldl f b xs = Array.foldl f b xs.toArray

@[inline]

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

Equations

• Vector.foldr f b xs = Array.foldr f b xs.toArray

@[inline]

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

Append two vectors.

Equations

• xs.append ys = { toArray := xs.toArray ++ ys.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) (xs : Vector α n) : Vector α m

Creates a vector from another with a provably equal length.

Equations

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

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

Equations

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

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

Equations

• xs.take i = { toArray := xs.take i, size_toArray := ⋯ }

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

Equations

• xs.drop i = { toArray := xs.drop i, size_toArray := ⋯ }

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

Equations

• xs.shrink i = { toArray := xs.shrink i, size_toArray := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

• xs.mapFinIdx f = { toArray := xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.size) => f i a ⋯, size_toArray := ⋯ }

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

Equations

• Vector.mapM f xs = Vector.mapM.go f xs 0 ⋯ { toArray := #[], size_toArray := ⋯ }

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

Equations

• Vector.mapM.go f xs k h acc = if h' : k < n then do let __do_lift ← f xs[k] Vector.mapM.go f xs (k + 1) ⋯ (acc.push __do_lift) else pure (Vector.cast ⋯ acc)

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

Equations

• xs.forM f = Array.forM f xs.toArray

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

Equations

• xs.flatMapM f = Vector.flatMapM.go xs f 0 ⋯ (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ })

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

Equations

• Vector.flatMapM.go xs f i h acc = if h' : i < n then do let __do_lift ← f xs[i] Vector.flatMapM.go xs f (i + 1) ⋯ (Vector.cast ⋯ (acc ++ __do_lift)) else pure (Vector.cast ⋯ acc)

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

Equations

• xs.mapFinIdxM f = Vector.mapFinIdxM.map xs f n 0 ⋯ (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ })

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

Equations

• Vector.mapFinIdxM.map xs f 0 j x ys_2 = pure ys_2
• Vector.mapFinIdxM.map xs f i_2.succ j inv_2 ys_2 = do let __do_lift ← f j xs[j] ⋯ Vector.mapFinIdxM.map xs f i_2 (j + 1) ⋯ (Vector.cast ⋯ (ys_2.push __do_lift))

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

Equations

• Vector.mapIdxM f xs = xs.mapFinIdxM fun (i : Nat) (a : α) (x : i < n) => f i a

@[inline]

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

Equations

• Vector.firstM f xs = Array.firstM f xs.toArray

@[inline]

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

Equations

• xs.flatten = { toArray := (Array.map Vector.toArray xs.toArray).flatten, size_toArray := ⋯ }

@[inline]

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

Equations

• xs.flatMap f = { toArray := Array.flatMap (fun (a : α) => (f a).toArray) xs.toArray, size_toArray := ⋯ }

@[inline]

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

Equations

• xs.zipIdx k = { toArray := xs.zipIdx k, size_toArray := ⋯ }

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

Equations

• @Vector.zipWithIndex = @Vector.zipIdx

@[inline]

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

Equations

• as.zip bs = { toArray := as.zip bs.toArray, size_toArray := ⋯ }

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

Equations

• Vector.zipWith f as bs = { toArray := Array.zipWith f as.toArray bs.toArray, size_toArray := ⋯ }

@[inline]

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

Equations

• xs.unzip = ({ toArray := xs.unzip.fst, size_toArray := ⋯ }, { toArray := xs.unzip.snd, 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} (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.

Equations

• xs.swap i j hi hj = { toArray := xs.swap i j ⋯ ⋯, size_toArray := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

• xs.swapAt! i x = ((xs.swapAt! i x).fst, { toArray := (xs.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.range' (start size : Nat) (step : Nat := 1) : Vector Nat size

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

Equations

• Vector.range' start size step = { toArray := Array.range' start size step, size_toArray := ⋯ }

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

Equations

• xs.isEqv ys r = xs.isEqvAux ys.toArray ⋯ r n ⋯

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

Equations

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

@[inline]

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

Reverse the elements of a vector.

Equations

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

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

Equations

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

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

Equations

• xs.eraseIdx! i = if x : i < n then xs.eraseIdx i x else let_fun this := { default := xs.pop }; panicWithPosWithDecl "Init.Data.Vector.Basic" "Vector.eraseIdx!" 362 4 "index 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.

Equations

• xs.insertIdx i x h = { toArray := xs.insertIdx i x ⋯, size_toArray := ⋯ }

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

Equations

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

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

Equations

• xs.tail = if x : 0 < n then xs.eraseIdx 0 x else Vector.cast ⋯ xs

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

Equations

• xs.finIdxOf? x = Option.map (Fin.cast ⋯) (xs.finIdxOf? x)

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

Equations

• @Vector.indexOf? = @Vector.finIdxOf?

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

Equations

• Vector.findFinIdx? p xs = Option.map (Fin.cast ⋯) (Array.findFinIdx? p xs.toArray)

@[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 contrained to Type here, to avoid having to have the predicate live in p : α → m (ULift Bool).

Equations

• Vector.findM? f as = Array.findM? f as.toArray

@[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 β)

Equations

• Vector.findSomeM? f as = Array.findSomeM? f as.toArray

@[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 contrained to Type here, to avoid having to have the predicate live in p : α → m (ULift Bool).

Equations

• Vector.findRevM? f as = Array.findRevM? f as.toArray

@[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 β)

Equations

• Vector.findSomeRevM? f as = Array.findSomeRevM? f as.toArray

@[inline]

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

Equations

• Vector.find? f as = Array.find? f as.toArray

@[inline]

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

Equations

• Vector.findRev? f as = Array.findRev? f as.toArray

@[inline]

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

Equations

• Vector.findSome? f as = Array.findSome? f as.toArray

@[inline]

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

Equations

• Vector.findSomeRev? f as = Array.findSomeRev? f as.toArray

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

Equations

• xs.isPrefixOf ys = xs.isPrefixOf ys.toArray

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

Equations

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

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

Equations

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

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

Equations

• xs.any p = xs.any p

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

Equations

• xs.all p = xs.all p

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

Equations

• Vector.countP p xs = Array.countP p xs.toArray

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

Equations

• Vector.count a xs = Array.count a xs.toArray

@[inline]

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

Equations

• xs.replace a b = { toArray := xs.replace a b, size_toArray := ⋯ }

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

Equations

• Vector.leftpad n a xs = Vector.cast ⋯ (Vector.mkVector (n - m) a ++ xs)

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

Equations

• Vector.rightpad n a xs = Vector.cast ⋯ (xs ++ Vector.mkVector (n - m) a)

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

Equations

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

ForM instance

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

Equations

• Vector.instForM = { forM := fun [Monad m] => Vector.forM }

@[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 α)

Equations

• Vector.instToStreamSubarray = { toStream := fun (xs : Vector α n) => xs.toSubarray 0 n }

Lexicographic ordering

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

Equations

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

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

Equations

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

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

Equations

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