theorem Array.of_push_eq_push {α : Type u_1} {a : α} {b : α} {as : Array α} {bs : Array α} (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 α) : (List.toArray as = List.toArray bs) = (as = bs)

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 }

Equations

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

@[irreducible]

def Array.mapM'.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) (as : Array α) (i : Nat) (acc : { bs : Array β // bs.size = i }) (hle : i ≤ as.size) : m { bs : Array β // bs.size = as.size }

Equations

• Array.mapM'.go f as i acc hle = if h : i = as.size then pure (h ▸ acc) else let_fun hlt := ⋯; do let b ← f as[i] Array.mapM'.go f as (i + 1) ⟨acc.val.push b, ⋯⟩ hlt

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

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

• as.mapMonoM f = Array.mapM f as

@[inline]

def Array.mapMono {α : Type u_1} (as : Array α) (f : α → α) : Array α

Equations

• as.mapMono f = (as.mapMonoM f).run