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.

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

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

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

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

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

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

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