source
theorem Array.of_push_eq_push {α : Type u_1} {a b : α} {as bs : Array α} (h : as.push a = bs.push b) :
as = bs ∧ a = b
source
theorem List.toArray_eq_toArray_eq {α : Type u_1} {as bs : List α} :
(as.toArray = bs.toArray) = (as = bs)
source
def Array.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) (as : Array α) :
m { bs : Array β // bs.size = as.size }

Applies the monadic action `f` to every element in the array, left-to-right, and returns the array of results. Furthermore, the resulting array's type guarantees that it contains the same number of elements as the input array.

Equations

- Array.mapM' f as = Array.mapM'.go✝ f as 0 ⟨Array.mkEmpty as.size, ⋯⟩ ⋯

Instances For

source
@[implemented_by _private.Init.Data.Array.BasicAux.0.mapMonoMImp]
def Array.mapMonoM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : Array α) (f : α → m α) :
m (Array α)

Applies a monadic function to each element of an array, returning the array of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new array if the result of each function call is pointer-equal to its argument.

Equations

- as.mapMonoM f = Array.mapM f as

Instances For

source
@[inline]
def Array.mapMono {α : Type u_1} (as : Array α) (f : α → α) :
Array α

Applies a function to each element of an array, returning the array of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new array if the result of each function call is pointer-equal to its argument.

Equations

- as.mapMono f = (as.mapMonoM fun (x : α) => pure (f x)).run

Instances For