Vectors

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

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

@[inline]

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

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

Equations

• xs.uset i v h = Vector.mk (xs.toArray.uset i v ⋯) ⋯

@[implemented_by _private.Batteries.Data.Vector.Basic.0.Vector.scanlMUnsafe]

def Vector.scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} [Monad m] (f : β → α → m β) (init : β) (as : Vector α n) : m (Vector β (n + 1))

Fold an effectful function f over the array from the left, returning the list of partial results.

Equations

• Vector.scanlM f init as = Vector.scanlM.loop f as init 0 ⋯ #v[]

@[irreducible]

def Vector.scanlM.loop {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} [Monad m] (f : β → α → m β) (as : Vector α n) (cur : β) (i : Nat) (hi : i ≤ n) (acc : Vector β i) : m (Vector β (n + 1))

Auxiliary tail-recursive function for scanlM

Equations

• Vector.scanlM.loop f as cur i hi acc = if h_lt : i < n then do let next ← f cur as[i] Vector.scanlM.loop f as next (i + 1) ⋯ (acc.push cur) else pure (Vector.cast ⋯ (acc.push cur))

@[implemented_by _private.Batteries.Data.Vector.Basic.0.Vector.scanrMUnsafe]

def Vector.scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] (f : α → β → m β) (init : β) (as : Vector α n) : m (Vector β (n + 1))

Fold an effectful function f over the array from the right, returning the list of partial results.

Equations

• Vector.scanrM f init as = Vector.scanrM.loop f as init n ⋯ (Vector.cast ⋯ #v[])

@[irreducible]

def Vector.scanrM.loop {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] (f : α → β → m β) (as : Vector α n) (cur : β) (i : Nat) (hi : i ≤ n) (acc : Vector β (n - i)) : m (Vector β (n + 1))

Auxiliary tail-recursive function for scanrM

Equations

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

@[inline]

def Vector.scanl {β : Type u_1} {α : Type u_2} {n : Nat} (f : β → α → β) (init : β) (as : Vector α n) : Vector β (n + 1)

Fold a function f over the list from the left, returning the vector of partial results.

Equations

• Vector.scanl f init as = (Vector.scanlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init as).run

@[inline]

def Vector.scanr {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → β → β) (init : β) (as : Vector α n) : Vector β (n + 1)

Fold a function f over the list from the right, returning the vector of partial results.

Equations

• Vector.scanr f init as = (Vector.scanrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init as).run