Documentation

Init.Data.Array.BasicAux

theorem Array.of_push_eq_push {α : Type u_1} {a : α} {b : α} {as : Array α} {bs : Array α} (h : Array.push as a = Array.push bs 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 β // Array.size bs = Array.size as }
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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 β // Array.size bs = i }) (hle : i Array.size as) :
    m { bs : Array β // Array.size bs = Array.size as }
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[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
      Instances For
        @[inline]
        def Array.mapMono {α : Type u_1} (as : Array α) (f : αα) :
        Equations
        Instances For