Documentation

Init.Data.Array.Basic

@[extern lean_mk_array]
def Array.mkArray {α : Type u} (n : Nat) (v : α) :
Equations
Instances For
    def Array.ofFn {α : Type u} {n : Nat} (f : Fin nα) :

    ofFn f with f : Fin n → α returns the list whose ith element is f i.

    ofFn f = #[f 0, f 1, ... , f(n - 1)]
    
    Equations
    Instances For
      @[irreducible]
      def Array.ofFn.go {α : Type u} {n : Nat} (f : Fin nα) (i : Nat) (acc : Array α) :

      Auxiliary for ofFn. ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]

      Equations
      Instances For

        The array #[0, 1, ..., n - 1].

        Equations
        Instances For
          @[simp]
          theorem Array.size_mkArray {α : Type u} (n : Nat) (v : α) :
          (mkArray n v).size = n
          Equations
          • Array.instEmptyCollection = { emptyCollection := #[] }
          instance Array.instInhabited {α : Type u} :
          Equations
          • Array.instInhabited = { default := #[] }
          def Array.isEmpty {α : Type u} (a : Array α) :
          Equations
          Instances For
            def Array.singleton {α : Type u} (v : α) :
            Equations
            Instances For
              @[extern lean_array_uget]
              def Array.uget {α : Type u} (a : Array α) (i : USize) (h : i.toNat < a.size) :
              α

              Low-level version of fget which is as fast as a C array read. Fin values are represented as tag pointers in the Lean runtime. Thus, fget may be slightly slower than uget.

              Equations
              • a.uget i h = a[i.toNat]
              Instances For
                instance Array.instGetElemUSizeLtNatToNatSize {α : Type u} :
                GetElem (Array α) USize α fun (xs : Array α) (i : USize) => i.toNat < xs.size
                Equations
                • Array.instGetElemUSizeLtNatToNatSize = { getElem := fun (xs : Array α) (i : USize) (h : i.toNat < xs.size) => xs.uget i h }
                def Array.back {α : Type u} [Inhabited α] (a : Array α) :
                α
                Equations
                • a.back = a.get! (a.size - 1)
                Instances For
                  def Array.get? {α : Type u} (a : Array α) (i : Nat) :
                  Equations
                  • a.get? i = if h : i < a.size then some a[i] else none
                  Instances For
                    def Array.back? {α : Type u} (a : Array α) :
                    Equations
                    • a.back? = a.get? (a.size - 1)
                    Instances For
                      @[reducible, inline]
                      abbrev Array.getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) :
                      α
                      Equations
                      • a.getLit i h₁ h₂ = let_fun this := ; a[i]
                      Instances For
                        @[simp]
                        theorem Array.size_set {α : Type u} (a : Array α) (i : Fin a.size) (v : α) :
                        (a.set i v).size = a.size
                        @[simp]
                        theorem Array.size_push {α : Type u} (a : Array α) (v : α) :
                        (a.push v).size = a.size + 1
                        @[extern lean_array_uset]
                        def Array.uset {α : Type u} (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) :

                        Low-level version of fset which is as fast as a C array fset. Fin values are represented as tag pointers in the Lean runtime. Thus, fset may be slightly slower than uset.

                        Equations
                        • a.uset i v h = a.set i.toNat, h v
                        Instances For
                          @[extern lean_array_fswap]
                          def Array.swap {α : Type u} (a : Array α) (i : Fin a.size) (j : Fin a.size) :

                          Swaps two entries in an array.

                          This will perform the update destructively provided that a has a reference count of 1 when called.

                          Equations
                          • a.swap i j = let v₁ := a.get i; let v₂ := a.get j; let a' := a.set i v₂; a'.set (j) v₁
                          Instances For
                            @[extern lean_array_swap]
                            def Array.swap! {α : Type u} (a : Array α) (i : Nat) (j : Nat) :

                            Swaps two entries in an array, or panics if either index is out of bounds.

                            This will perform the update destructively provided that a has a reference count of 1 when called.

                            Equations
                            • a.swap! i j = if h₁ : i < a.size then if h₂ : j < a.size then a.swap i, h₁ j, h₂ else a else a
                            Instances For
                              @[inline]
                              def Array.swapAt {α : Type u} (a : Array α) (i : Fin a.size) (v : α) :
                              α × Array α
                              Equations
                              • a.swapAt i v = let e := a.get i; let a := a.set i v; (e, a)
                              Instances For
                                @[inline]
                                def Array.swapAt! {α : Type u} (a : Array α) (i : Nat) (v : α) :
                                α × Array α
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[extern lean_array_pop]
                                  def Array.pop {α : Type u} (a : Array α) :
                                  Equations
                                  • a.pop = { data := a.data.dropLast }
                                  Instances For
                                    def Array.shrink {α : Type u} (a : Array α) (n : Nat) :
                                    Equations
                                    Instances For
                                      def Array.shrink.loop {α : Type u} :
                                      NatArray αArray α
                                      Equations
                                      Instances For
                                        @[inline]
                                        unsafe def Array.modifyMUnsafe {α : Type u} {m : Type u → Type u_1} [Monad m] (a : Array α) (i : Nat) (f : αm α) :
                                        m (Array α)
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[implemented_by Array.modifyMUnsafe]
                                          def Array.modifyM {α : Type u} {m : Type u → Type u_1} [Monad m] (a : Array α) (i : Nat) (f : αm α) :
                                          m (Array α)
                                          Equations
                                          • a.modifyM i f = if h : i < a.size then let idx := i, h; let v := a.get idx; do let vf v pure (a.set idx v) else pure a
                                          Instances For
                                            @[inline]
                                            def Array.modify {α : Type u} (a : Array α) (i : Nat) (f : αα) :
                                            Equations
                                            • a.modify i f = (a.modifyM i f).run
                                            Instances For
                                              @[inline]
                                              def Array.modifyOp {α : Type u} (self : Array α) (idx : Nat) (f : αα) :
                                              Equations
                                              • self.modifyOp idx f = self.modify idx f
                                              Instances For
                                                @[inline]
                                                unsafe def Array.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : αβm (ForInStep β)) :
                                                m β

                                                We claim this unsafe implementation is correct because an array cannot have more than usizeSz elements in our runtime.

                                                This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies as.size < usizeSz to true.

                                                Equations
                                                Instances For
                                                  @[specialize #[]]
                                                  unsafe def Array.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αβm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
                                                  m β
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[implemented_by Array.forInUnsafe]
                                                    def Array.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : αβm (ForInStep β)) :
                                                    m β

                                                    Reference implementation for forIn

                                                    Equations
                                                    Instances For
                                                      def Array.forIn.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αβm (ForInStep β)) (i : Nat) (h : i as.size) (b : β) :
                                                      m β
                                                      Equations
                                                      Instances For
                                                        instance Array.instForIn {α : Type u} {m : Type u_1 → Type u_2} :
                                                        ForIn m (Array α) α
                                                        Equations
                                                        • Array.instForIn = { forIn := fun {β : Type u_1} [Monad m] => Array.forIn }
                                                        @[inline]
                                                        unsafe def Array.foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : βαm β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                        m β

                                                        See comment at forInUnsafe

                                                        Equations
                                                        Instances For
                                                          @[specialize #[]]
                                                          unsafe def Array.foldlMUnsafe.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : βαm β) (as : Array α) (i : USize) (stop : USize) (b : β) :
                                                          m β
                                                          Equations
                                                          Instances For
                                                            @[implemented_by Array.foldlMUnsafe]
                                                            def Array.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : βαm β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                            m β

                                                            Reference implementation for foldlM

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def Array.foldlM.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : βαm β) (as : Array α) (stop : Nat) (h : stop as.size) (i : Nat) (j : Nat) (b : β) :
                                                              m β
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[inline]
                                                                unsafe def Array.foldrMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αβm β) (init : β) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) :
                                                                m β

                                                                See comment at forInUnsafe

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[specialize #[]]
                                                                  unsafe def Array.foldrMUnsafe.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αβm β) (as : Array α) (i : USize) (stop : USize) (b : β) :
                                                                  m β
                                                                  Equations
                                                                  Instances For
                                                                    @[implemented_by Array.foldrMUnsafe]
                                                                    def Array.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αβm β) (init : β) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) :
                                                                    m β

                                                                    Reference implementation for foldrM

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      def Array.foldrM.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αβm β) (as : Array α) (stop : optParam Nat 0) (i : Nat) (h : i as.size) (b : β) :
                                                                      m β
                                                                      Equations
                                                                      Instances For
                                                                        @[inline]
                                                                        unsafe def Array.mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm β) (as : Array α) :
                                                                        m (Array β)

                                                                        See comment at forInUnsafe

                                                                        Equations
                                                                        Instances For
                                                                          @[specialize #[]]
                                                                          unsafe def Array.mapMUnsafe.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm β) (sz : USize) (i : USize) (r : Array NonScalar) :
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[implemented_by Array.mapMUnsafe]
                                                                            def Array.mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm β) (as : Array α) :
                                                                            m (Array β)

                                                                            Reference implementation for mapM

                                                                            Equations
                                                                            Instances For
                                                                              @[irreducible]
                                                                              def Array.mapM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm β) (as : Array α) (i : Nat) (r : Array β) :
                                                                              m (Array β)
                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                def Array.mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.sizeαm β) :
                                                                                m (Array β)
                                                                                Equations
                                                                                Instances For
                                                                                  @[specialize #[]]
                                                                                  def Array.mapIdxM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.sizeαm β) (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) :
                                                                                  m (Array β)
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Array.findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αm (Option β)) :
                                                                                    m (Option β)
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Array.findM? {α : Type} {m : TypeType} [Monad m] (as : Array α) (p : αm Bool) :
                                                                                      m (Option α)
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        def Array.findIdxM? {α : Type u} {m : TypeType u_1} [Monad m] (as : Array α) (p : αm Bool) :
                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          unsafe def Array.anyMUnsafe {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            @[specialize #[]]
                                                                                            unsafe def Array.anyMUnsafe.any {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (i : USize) (stop : USize) :
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[implemented_by Array.anyMUnsafe]
                                                                                              def Array.anyM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                              Equations
                                                                                              • Array.anyM p as start stop = let any := fun (stop : Nat) (h : stop as.size) => Array.anyM.loop p as stop h start; if h : stop as.size then any stop h else any as.size
                                                                                              Instances For
                                                                                                @[irreducible]
                                                                                                def Array.anyM.loop {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (stop : Nat) (h : stop as.size) (j : Nat) :
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Array.allM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    def Array.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αm (Option β)) :
                                                                                                    m (Option β)
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[specialize #[]]
                                                                                                      def Array.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αm (Option β)) (i : Nat) :
                                                                                                      i as.sizem (Option β)
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        def Array.findRevM? {α : Type} {m : TypeType w} [Monad m] (as : Array α) (p : αm Bool) :
                                                                                                        m (Option α)
                                                                                                        Equations
                                                                                                        • as.findRevM? p = as.findSomeRevM? fun (a : α) => do let __do_liftp a pure (if __do_lift = true then some a else none)
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          def Array.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            def Array.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) :
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              def Array.foldl {α : Type u} {β : Type v} (f : βαβ) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                              β
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                def Array.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) :
                                                                                                                β
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  def Array.map {α : Type u} {β : Type v} (f : αβ) (as : Array α) :
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def Array.mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.sizeαβ) :
                                                                                                                    Equations
                                                                                                                    • as.mapIdx f = (as.mapIdxM f).run
                                                                                                                    Instances For
                                                                                                                      def Array.zipWithIndex {α : Type u} (arr : Array α) :
                                                                                                                      Array (α × Nat)

                                                                                                                      Turns #[a, b] into #[(a, 0), (b, 1)].

                                                                                                                      Equations
                                                                                                                      • arr.zipWithIndex = arr.mapIdx fun (i : Fin arr.size) (a : α) => (a, i)
                                                                                                                      Instances For
                                                                                                                        @[inline]
                                                                                                                        def Array.find? {α : Type} (as : Array α) (p : αBool) :
                                                                                                                        Equations
                                                                                                                        • as.find? p = (as.findM? p).run
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          def Array.findSome? {α : Type u} {β : Type v} (as : Array α) (f : αOption β) :
                                                                                                                          Equations
                                                                                                                          • as.findSome? f = (as.findSomeM? f).run
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            def Array.findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : αOption β) :
                                                                                                                            β
                                                                                                                            Equations
                                                                                                                            • a.findSome! f = match a.findSome? f with | some b => b | none => panicWithPosWithDecl "Init.Data.Array.Basic" "Array.findSome!" 450 14 "failed to find element"
                                                                                                                            Instances For
                                                                                                                              @[inline]
                                                                                                                              def Array.findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : αOption β) :
                                                                                                                              Equations
                                                                                                                              • as.findSomeRev? f = (as.findSomeRevM? f).run
                                                                                                                              Instances For
                                                                                                                                @[inline]
                                                                                                                                def Array.findRev? {α : Type} (as : Array α) (p : αBool) :
                                                                                                                                Equations
                                                                                                                                • as.findRev? p = (as.findRevM? p).run
                                                                                                                                Instances For
                                                                                                                                  @[inline]
                                                                                                                                  def Array.findIdx? {α : Type u} (as : Array α) (p : αBool) :
                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    @[irreducible]
                                                                                                                                    def Array.findIdx?.loop {α : Type u} (as : Array α) (p : αBool) (j : Nat) :
                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      def Array.getIdx? {α : Type u} [BEq α] (a : Array α) (v : α) :
                                                                                                                                      Equations
                                                                                                                                      • a.getIdx? v = a.findIdx? fun (a : α) => a == v
                                                                                                                                      Instances For
                                                                                                                                        @[inline]
                                                                                                                                        def Array.any {α : Type u} (as : Array α) (p : αBool) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline]
                                                                                                                                          def Array.all {α : Type u} (as : Array α) (p : αBool) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            def Array.contains {α : Type u} [BEq α] (as : Array α) (a : α) :
                                                                                                                                            Equations
                                                                                                                                            • as.contains a = as.any (fun (x : α) => x == a) 0
                                                                                                                                            Instances For
                                                                                                                                              def Array.elem {α : Type u} [BEq α] (a : α) (as : Array α) :
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                def Array.getEvenElems {α : Type u} (as : Array α) :
                                                                                                                                                Equations
                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                Instances For
                                                                                                                                                  @[export lean_array_to_list]
                                                                                                                                                  def Array.toList {α : Type u} (as : Array α) :
                                                                                                                                                  List α

                                                                                                                                                  Convert a Array α into an List α. This is O(n) in the size of the array.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[inline]
                                                                                                                                                    def Array.toListAppend {α : Type u} (as : Array α) (l : List α) :
                                                                                                                                                    List α

                                                                                                                                                    Prepends an Array α onto the front of a list. Equivalent to as.toList ++ l.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      instance Array.instRepr {α : Type u} [Repr α] :
                                                                                                                                                      Repr (Array α)
                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      instance Array.instToString {α : Type u} [ToString α] :
                                                                                                                                                      Equations
                                                                                                                                                      • Array.instToString = { toString := fun (a : Array α) => "#" ++ toString a.toList }
                                                                                                                                                      def Array.append {α : Type u} (as : Array α) (bs : Array α) :
                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        instance Array.instAppend {α : Type u} :
                                                                                                                                                        Equations
                                                                                                                                                        • Array.instAppend = { append := Array.append }
                                                                                                                                                        def Array.appendList {α : Type u} (as : Array α) (bs : List α) :
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          instance Array.instHAppendList {α : Type u} :
                                                                                                                                                          HAppend (Array α) (List α) (Array α)
                                                                                                                                                          Equations
                                                                                                                                                          • Array.instHAppendList = { hAppend := Array.appendList }
                                                                                                                                                          @[inline]
                                                                                                                                                          def Array.concatMapM {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : αm (Array β)) (as : Array α) :
                                                                                                                                                          m (Array β)
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            def Array.concatMap {α : Type u} {β : Type u_1} (f : αArray β) (as : Array α) :
                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              def Array.flatten {α : Type u} (as : Array (Array α)) :

                                                                                                                                                              Joins array of array into a single array.

                                                                                                                                                              flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯] = #[a₁, a₂, ⋯, b₁, b₂, ⋯]

                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For
                                                                                                                                                                  @[irreducible, specialize #[]]
                                                                                                                                                                  def Array.isEqvAux {α : Type u_1} (a : Array α) (b : Array α) (hsz : a.size = b.size) (p : ααBool) (i : Nat) :
                                                                                                                                                                  Equations
                                                                                                                                                                  • a.isEqvAux b hsz p i = if h : i < a.size then let_fun this := ; p a[i] b[i] && a.isEqvAux b hsz p (i + 1) else true
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    def Array.isEqv {α : Type u_1} (a : Array α) (b : Array α) (p : ααBool) :
                                                                                                                                                                    Equations
                                                                                                                                                                    • a.isEqv b p = if h : a.size = b.size then a.isEqvAux b h p 0 else false
                                                                                                                                                                    Instances For
                                                                                                                                                                      instance Array.instBEq {α : Type u_1} [BEq α] :
                                                                                                                                                                      BEq (Array α)
                                                                                                                                                                      Equations
                                                                                                                                                                      • Array.instBEq = { beq := fun (a b : Array α) => a.isEqv b BEq.beq }
                                                                                                                                                                      @[inline]
                                                                                                                                                                      def Array.filter {α : Type u_1} (p : αBool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]
                                                                                                                                                                        def Array.filterM {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                                                                                        m (Array α)
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[specialize #[]]
                                                                                                                                                                          def Array.filterMapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm (Option β)) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                                                                                          m (Array β)
                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            def Array.filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[specialize #[]]
                                                                                                                                                                              def Array.getMax? {α : Type u_1} (as : Array α) (lt : ααBool) :
                                                                                                                                                                              Equations
                                                                                                                                                                              • as.getMax? lt = if h : 0 < as.size then let a0 := as[0]; some (Array.foldl (fun (best a : α) => if lt best a = true then a else best) a0 as 1) else none
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[inline]
                                                                                                                                                                                def Array.partition {α : Type u_1} (p : αBool) (as : Array α) :
                                                                                                                                                                                Array α × Array α
                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For
                                                                                                                                                                                  theorem Array.ext {α : Type u_1} (a : Array α) (b : Array α) (h₁ : a.size = b.size) (h₂ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), a[i] = b[i]) :
                                                                                                                                                                                  a = b
                                                                                                                                                                                  theorem Array.ext.extAux {α : Type u_1} (a : List α) (b : List α) (h₁ : a.length = b.length) (h₂ : ∀ (i : Nat) (hi₁ : i < a.length) (hi₂ : i < b.length), a.get i, hi₁ = b.get i, hi₂) :
                                                                                                                                                                                  a = b
                                                                                                                                                                                  theorem Array.extLit {α : Type u_1} {n : Nat} (a : Array α) (b : Array α) (hsz₁ : a.size = n) (hsz₂ : b.size = n) (h : ∀ (i : Nat) (hi : i < n), a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) :
                                                                                                                                                                                  a = b
                                                                                                                                                                                  @[irreducible]
                                                                                                                                                                                  def Array.indexOfAux {α : Type u_1} [BEq α] (a : Array α) (v : α) (i : Nat) :
                                                                                                                                                                                  Option (Fin a.size)
                                                                                                                                                                                  Equations
                                                                                                                                                                                  • a.indexOfAux v i = if h : i < a.size then let idx := i, h; if (a.get idx == v) = true then some idx else a.indexOfAux v (i + 1) else none
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    def Array.indexOf? {α : Type u_1} [BEq α] (a : Array α) (v : α) :
                                                                                                                                                                                    Option (Fin a.size)
                                                                                                                                                                                    Equations
                                                                                                                                                                                    • a.indexOf? v = a.indexOfAux v 0
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem Array.size_swap {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Fin a.size) :
                                                                                                                                                                                      (a.swap i j).size = a.size
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem Array.size_pop {α : Type u_1} (a : Array α) :
                                                                                                                                                                                      a.pop.size = a.size - 1
                                                                                                                                                                                      theorem Array.reverse.termination {i : Nat} {j : Nat} (h : i < j) :
                                                                                                                                                                                      j - 1 - (i + 1) < j - i
                                                                                                                                                                                      def Array.reverse {α : Type u_1} (as : Array α) :
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[irreducible]
                                                                                                                                                                                        def Array.reverse.loop {α : Type u_1} (as : Array α) (i : Nat) (j : Fin as.size) :
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[irreducible]
                                                                                                                                                                                          def Array.popWhile {α : Type u_1} (p : αBool) (as : Array α) :
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            def Array.takeWhile {α : Type u_1} (p : αBool) (as : Array α) :
                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[irreducible]
                                                                                                                                                                                              def Array.takeWhile.go {α : Type u_1} (p : αBool) (as : Array α) (i : Nat) (r : Array α) :
                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[irreducible]
                                                                                                                                                                                                def Array.feraseIdx {α : Type u_1} (a : Array α) (i : Fin a.size) :

                                                                                                                                                                                                Remove the element at a given index from an array without bounds checks, using a Fin index.

                                                                                                                                                                                                This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                • a.feraseIdx i = if h : i + 1 < a.size then let a' := a.swap i + 1, h i; let i' := i + 1, ; a'.feraseIdx i' else a.pop
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  theorem Array.size_feraseIdx {α : Type u_1} (a : Array α) (i : Fin a.size) :
                                                                                                                                                                                                  (a.feraseIdx i).size = a.size - 1
                                                                                                                                                                                                  def Array.eraseIdx {α : Type u_1} (a : Array α) (i : Nat) :

                                                                                                                                                                                                  Remove the element at a given index from an array, or do nothing if the index is out of bounds.

                                                                                                                                                                                                  This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • a.eraseIdx i = if h : i < a.size then a.feraseIdx i, h else a
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    def Array.erase {α : Type u_1} [BEq α] (as : Array α) (a : α) :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • as.erase a = match as.indexOf? a with | none => as | some i => as.feraseIdx i
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                      def Array.insertAt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (a : α) :

                                                                                                                                                                                                      Insert element a at position i.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      • as.insertAt i a = let j := as.size; let as_1 := as.push a; Array.insertAt.loop as i as_1 j,
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[irreducible]
                                                                                                                                                                                                        def Array.insertAt.loop {α : Type u_1} (as : Array α) (i : Fin (as✝.size + 1)) (as : Array α) (j : Fin as.size) :
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          def Array.insertAt! {α : Type u_1} (as : Array α) (i : Nat) (a : α) :

                                                                                                                                                                                                          Insert element a at position i. Panics if i is not i ≤ as.size.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          • as.insertAt! i a = if h : i as.size then as.insertAt i, a else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.insertAt!" 780 7 "invalid index"
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            def Array.toListLitAux {α : Type u_1} (a : Array α) (n : Nat) (hsz : a.size = n) (i : Nat) :
                                                                                                                                                                                                            i a.sizeList αList α
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • a.toListLitAux n hsz 0 x_3 x = x
                                                                                                                                                                                                            • a.toListLitAux n hsz i.succ hi x = a.toListLitAux n hsz i (a.getLit i hsz :: x)
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def Array.toArrayLit {α : Type u_1} (a : Array α) (n : Nat) (hsz : a.size = n) :
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • a.toArrayLit n hsz = List.toArray (a.toListLitAux n hsz n [])
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                theorem Array.ext' {α : Type u_1} {as : Array α} {bs : Array α} (h : as.data = bs.data) :
                                                                                                                                                                                                                as = bs
                                                                                                                                                                                                                @[simp]
                                                                                                                                                                                                                theorem Array.toArrayAux_eq {α : Type u_1} (as : List α) (acc : Array α) :
                                                                                                                                                                                                                (as.toArrayAux acc).data = acc.data ++ as
                                                                                                                                                                                                                @[simp]
                                                                                                                                                                                                                theorem Array.data_toArray {α : Type u_1} (as : List α) :
                                                                                                                                                                                                                (List.toArray as).data = as
                                                                                                                                                                                                                theorem Array.toArrayLit_eq {α : Type u_1} (as : Array α) (n : Nat) (hsz : as.size = n) :
                                                                                                                                                                                                                as = as.toArrayLit n hsz
                                                                                                                                                                                                                theorem Array.toArrayLit_eq.getLit_eq {α : Type u_1} (n : Nat) (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) :
                                                                                                                                                                                                                as.getLit i h₁ h₂ = as.data[i]
                                                                                                                                                                                                                theorem Array.toArrayLit_eq.go {α : Type u_1} (as : Array α) (n : Nat) (hsz : as.size = n) (i : Nat) (hi : i as.size) :
                                                                                                                                                                                                                as.toListLitAux n hsz i hi (List.drop i as.data) = as.data
                                                                                                                                                                                                                @[irreducible]
                                                                                                                                                                                                                def Array.isPrefixOfAux {α : Type u_1} [BEq α] (as : Array α) (bs : Array α) (hle : as.size bs.size) (i : Nat) :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • as.isPrefixOfAux bs hle i = if h : i < as.size then let a := as[i]; let_fun this := ; let b := bs[i]; if (a == b) = true then as.isPrefixOfAux bs hle (i + 1) else false else true
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  def Array.isPrefixOf {α : Type u_1} [BEq α] (as : Array α) (bs : Array α) :

                                                                                                                                                                                                                  Return true iff as is a prefix of bs. That is, bs = as ++ t for some t : List α.

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  • as.isPrefixOf bs = if h : as.size bs.size then as.isPrefixOfAux bs h 0 else false
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    def Array.allDiff {α : Type u_1} [BEq α] (as : Array α) :
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      @[irreducible, specialize #[]]
                                                                                                                                                                                                                      def Array.zipWithAux {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                        def Array.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : αβγ) :
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          def Array.zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :
                                                                                                                                                                                                                          Array (α × β)
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • as.zip bs = as.zipWith bs Prod.mk
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            def Array.unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) :
                                                                                                                                                                                                                            Array α × Array β
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              def Array.split {α : Type u_1} (as : Array α) (p : αBool) :
                                                                                                                                                                                                                              Array α × Array α
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • as.split p = Array.foldl (fun (x : Array α × Array α) (a : α) => match x with | (as, bs) => if p a = true then (as.push a, bs) else (as, bs.push a)) (#[], #[]) as 0
                                                                                                                                                                                                                              Instances For