# Documentation

## Init.Data.Array.BasicAux

theorem Array.of_push_eq_push {α : Type u_1} {a : α} {b : α} {as : } {bs : } (h : as.push a = bs.push b) :
as = bs a = b
@[simp]
theorem List.toArray_eq_toArray_eq {α : Type u_1} (as : List α) (bs : List α) :
() = (as = bs)
def Array.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αm β) (as : ) :
m { bs : // bs.size = as.size }
Equations
Instances For
def Array.mapM'.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αm β) (as : ) (i : Nat) (acc : { bs : // bs.size = i }) (hle : i as.size) :
m { bs : // bs.size = as.size }
Equations
• Array.mapM'.go f as i acc hle = if h : i = as.size then pure (hacc) else let_fun hlt := ; do let bf as[i] Array.mapM'.go f as (i + 1) acc.val.push b, hlt
Instances For
@[implemented_by _private.Init.Data.Array.BasicAux.0.mapMonoMImp]
def Array.mapMonoM {m : Type u_1 → Type u_2} {α : Type u_1} [] (as : ) (f : αm α) :
m ()

Monomorphic Array.mapM. The internal implementation uses pointer equality, and does not allocate a new array if the result of each f a is a pointer equal value a.

Equations
Instances For
@[inline]
def Array.mapMono {α : Type u_1} (as : ) (f : αα) :
Equations
• as.mapMono f = (as.mapMonoM f).run
Instances For