Documentation

Init.Data.Array.Basic

Array literal syntax #

Syntax for Array α.

Conventions for notations in identifiers:

  • The recommended spelling of #[] in identifiers is empty.

  • The recommended spelling of #[x] in identifiers is singleton.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[reducible, inline, deprecated Array.toList (since := "2024-09-10")]
    abbrev Array.data {α : Type u_1} (self : Array α) :
    List α
    Equations
    Instances For

      Preliminary theorems #

      @[simp]
      theorem Array.size_set {α : Type u} {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
      (xs.set i v h).size = xs.size
      @[simp]
      theorem Array.size_push {α : Type u} {xs : Array α} (v : α) :
      (xs.push v).size = xs.size + 1
      theorem Array.ext {α : Type u} {xs ys : Array α} (h₁ : xs.size = ys.size) (h₂ : ∀ (i : Nat) (hi₁ : i < xs.size) (hi₂ : i < ys.size), xs[i] = ys[i]) :
      xs = ys
      theorem Array.ext.extAux {α : Type u} (as bs : List α) (h₁ : as.length = bs.length) (h₂ : ∀ (i : Nat) (hi₁ : i < as.length) (hi₂ : i < bs.length), as[i] = bs[i]) :
      as = bs
      theorem Array.ext' {α : Type u} {xs ys : Array α} (h : xs.toList = ys.toList) :
      xs = ys
      @[simp]
      theorem Array.toArrayAux_eq {α : Type u} {as : List α} {acc : Array α} :
      (as.toArrayAux acc).toList = acc.toList ++ as
      @[simp]
      theorem Array.toArray_toList {α : Type u} {xs : Array α} :
      @[simp]
      theorem Array.getElem_toList {α : Type u} {xs : Array α} {i : Nat} (h : i < xs.size) :
      xs.toList[i] = xs[i]
      @[simp]
      theorem Array.getElem?_toList {α : Type u} {xs : Array α} {i : Nat} :
      xs.toList[i]? = xs[i]?
      structure Array.Mem {α : Type u} (as : Array α) (a : α) :

      a ∈ as is a predicate which asserts that a is in the array as.

      Instances For
        instance Array.instMembership {α : Type u} :
        Equations
        theorem Array.mem_def {α : Type u} {a : α} {as : Array α} :
        a as a as.toList
        @[simp]
        theorem Array.mem_toArray {α : Type u} {a : α} {l : List α} :
        a l.toArray a l
        @[simp]
        theorem Array.getElem_mem {α : Type u} {xs : Array α} {i : Nat} (h : i < xs.size) :
        xs[i] xs
        @[reducible, inline, deprecated Array.toArray_toList (since := "2025-02-17")]
        abbrev List.toArray_toList {α : Type u_1} {xs : Array α} :
        Equations
        Instances For
          theorem List.toList_toArray {α : Type u} {as : List α} :
          @[reducible, inline, deprecated List.toList_toArray (since := "2025-02-17")]
          abbrev Array.toList_toArray {α : Type u_1} {as : List α} :
          Equations
          Instances For
            @[simp]
            theorem List.size_toArray {α : Type u} {as : List α} :
            @[reducible, inline, deprecated List.size_toArray (since := "2025-02-17")]
            abbrev Array.size_toArray {α : Type u_1} {as : List α} :
            Equations
            Instances For
              @[simp]
              theorem List.getElem_toArray {α : Type u} {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
              xs.toArray[i] = xs[i]
              @[simp]
              theorem List.getElem?_toArray {α : Type u} {xs : List α} {i : Nat} :
              @[simp]
              theorem List.getElem!_toArray {α : Type u} [Inhabited α] {xs : List α} {i : Nat} :
              theorem Array.size_eq_length_toList {α : Type u} {xs : Array α} :
              @[reducible, inline, deprecated Array.toList_toArray (since := "2024-09-09")]
              abbrev Array.data_toArray {α : Type u_1} {as : List α} :
              Equations
              Instances For

                Externs #

                @[extern lean_array_size]
                def Array.usize {α : Type u} (a : Array α) :

                Returns the size of the array as a platform-native unsigned integer.

                This is a low-level version of Array.size that directly queries the runtime system's representation of arrays. While this is not provable, Array.usize always returns the exact size of the array since the implementation only supports arrays of size less than USize.size.

                Equations
                Instances For
                  @[extern lean_array_uget]
                  def Array.uget {α : Type u} (a : Array α) (i : USize) (h : i.toNat < a.size) :
                  α

                  Low-level indexing operator which is as fast as a C array read.

                  This avoids overhead due to unboxing a Nat used as an index.

                  Equations
                  Instances For
                    @[extern lean_array_uset]
                    def Array.uset {α : Type u} (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) :

                    Low-level modification operator which is as fast as a C array write. The modification is performed in-place when the reference to the array is unique.

                    This avoids overhead due to unboxing a Nat used as an index.

                    Equations
                    Instances For
                      @[extern lean_array_pop]
                      def Array.pop {α : Type u} (xs : Array α) :

                      Removes the last element of an array. If the array is empty, then it is returned unmodified. The modification is performed in-place when the reference to the array is unique.

                      Examples:

                      • #[1, 2, 3].pop = #[1, 2]
                      • #["orange", "yellow"].pop = #["orange"]
                      • (#[] : Array String).pop = #[]
                      Equations
                      Instances For
                        @[simp]
                        theorem Array.size_pop {α : Type u} {xs : Array α} :
                        xs.pop.size = xs.size - 1
                        @[extern lean_mk_array]
                        def Array.replicate {α : Type u} (n : Nat) (v : α) :

                        Creates an array that contains n repetitions of v.

                        The corresponding List function is List.replicate.

                        Examples:

                        Equations
                        Instances For
                          @[extern lean_mk_array, deprecated Array.replicate (since := "2025-03-18")]
                          def Array.mkArray {α : Type u} (n : Nat) (v : α) :

                          Creates an array that contains n repetitions of v.

                          The corresponding List function is List.replicate.

                          Examples:

                          Equations
                          Instances For
                            @[extern lean_array_fswap]
                            def Array.swap {α : Type u} (xs : Array α) (i j : Nat) (hi : i < xs.size := by get_elem_tactic) (hj : j < xs.size := by get_elem_tactic) :

                            Swaps two elements of an array. The modification is performed in-place when the reference to the array is unique.

                            Examples:

                            • #["red", "green", "blue", "brown"].swap 0 3 = #["brown", "green", "blue", "red"]
                            • #["red", "green", "blue", "brown"].swap 0 2 = #["blue", "green", "red", "brown"]
                            • #["red", "green", "blue", "brown"].swap 1 2 = #["red", "blue", "green", "brown"]
                            • #["red", "green", "blue", "brown"].swap 3 0 = #["brown", "green", "blue", "red"]
                            Equations
                            Instances For
                              @[simp]
                              theorem Array.size_swap {α : Type u} {xs : Array α} {i j : Nat} {hi : i < xs.size} {hj : j < xs.size} :
                              (xs.swap i j hi hj).size = xs.size
                              @[extern lean_array_swap]
                              def Array.swapIfInBounds {α : Type u} (xs : Array α) (i j : Nat) :

                              Swaps two elements of an array, returning the array unchanged if either index is out of bounds. The modification is performed in-place when the reference to the array is unique.

                              Examples:

                              • #["red", "green", "blue", "brown"].swapIfInBounds 0 3 = #["brown", "green", "blue", "red"]
                              • #["red", "green", "blue", "brown"].swapIfInBounds 0 2 = #["blue", "green", "red", "brown"]
                              • #["red", "green", "blue", "brown"].swapIfInBounds 1 2 = #["red", "blue", "green", "brown"]
                              • #["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]
                              • #["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]
                              Equations
                              Instances For
                                @[reducible, inline, deprecated Array.swapIfInBounds (since := "2024-11-24")]
                                abbrev Array.swap! {α : Type u_1} (xs : Array α) (i j : Nat) :
                                Equations
                                Instances For

                                  GetElem instance for USize, backed by uget #

                                  instance Array.instGetElemUSizeLtNatToNatSize {α : Type u} :
                                  GetElem (Array α) USize α fun (xs : Array α) (i : USize) => i.toNat < xs.size
                                  Equations

                                  Definitions #

                                  Equations
                                  instance Array.instInhabited {α : Type u} :
                                  Equations
                                  def Array.isEmpty {α : Type u} (xs : Array α) :

                                  Checks whether an array is empty.

                                  An array is empty if its size is 0.

                                  Examples:

                                  Equations
                                  Instances For
                                    @[specialize #[]]
                                    def Array.isEqvAux {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : ααBool) (i : Nat) :
                                    i xs.sizeBool
                                    Equations
                                    Instances For
                                      @[inline]
                                      def Array.isEqv {α : Type u} (xs ys : Array α) (p : ααBool) :

                                      Returns true if as and bs have the same length and they are pairwise related by eqv.

                                      Short-circuits at the first non-related pair of elements.

                                      Examples:

                                      • #[1, 2, 3].isEqv #[2, 3, 4] (· < ·) = true
                                      • #[1, 2, 3].isEqv #[2, 2, 4] (· < ·) = false
                                      • #[1, 2, 3].isEqv #[2, 3] (· < ·) = false
                                      Equations
                                      Instances For
                                        instance Array.instBEq {α : Type u} [BEq α] :
                                        BEq (Array α)
                                        Equations
                                        def Array.ofFn {α : Type u} {n : Nat} (f : Fin nα) :

                                        Creates an array by applying f to each potential index in order, starting at 0.

                                        Examples:

                                        • Array.ofFn (n := 3) toString = #["0", "1", "2"]
                                        • Array.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = #["red", "green", "blue"]
                                        Equations
                                        Instances For
                                          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

                                            Constructs an array that contains all the numbers from 0 to n, exclusive.

                                            Examples:

                                            Equations
                                            Instances For
                                              def Array.range' (start size : Nat) (step : Nat := 1) :

                                              Constructs an array of numbers of size size, starting at start and increasing by step at each element.

                                              In other words, Array.range' start size step is #[start, start+step, ..., start+(len-1)*step].

                                              Examples:

                                              Equations
                                              Instances For
                                                @[inline]
                                                def Array.singleton {α : Type u} (v : α) :

                                                Constructs a single-element array that contains v.

                                                Examples:

                                                Equations
                                                Instances For
                                                  def Array.back! {α : Type u} [Inhabited α] (xs : Array α) :
                                                  α

                                                  Returns the last element of an array, or panics if the array is empty.

                                                  Safer alternatives include Array.back, which requires a proof the array is non-empty, and Array.back?, which returns an Option.

                                                  Equations
                                                  Instances For
                                                    def Array.back {α : Type u} (xs : Array α) (h : 0 < xs.size := by get_elem_tactic) :
                                                    α

                                                    Returns the last element of an array, given a proof that the array is not empty.

                                                    See Array.back! for the version that panics if the array is empty, or Array.back? for the version that returns an option.

                                                    Equations
                                                    Instances For
                                                      def Array.back? {α : Type u} (xs : Array α) :

                                                      Returns the last element of an array, or none if the array is empty.

                                                      See Array.back! for the version that panics if the array is empty, or Array.back for the version that requires a proof the array is non-empty.

                                                      Equations
                                                      Instances For
                                                        @[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
                                                        def Array.get? {α : Type u} (xs : Array α) (i : Nat) :
                                                        Equations
                                                        Instances For
                                                          @[inline]
                                                          def Array.swapAt {α : Type u} (xs : Array α) (i : Nat) (v : α) (hi : i < xs.size := by get_elem_tactic) :
                                                          α × Array α

                                                          Swaps a new element with the element at the given index.

                                                          Returns the value formerly found at i, paired with an array in which the value at i has been replaced with v.

                                                          Examples:

                                                          • #["spinach", "broccoli", "carrot"].swapAt 1 "pepper" = ("broccoli", #["spinach", "pepper", "carrot"])
                                                          • #["spinach", "broccoli", "carrot"].swapAt 2 "pepper" = ("carrot", #["spinach", "broccoli", "pepper"])
                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def Array.swapAt! {α : Type u} (xs : Array α) (i : Nat) (v : α) :
                                                            α × Array α

                                                            Swaps a new element with the element at the given index. Panics if the index is out of bounds.

                                                            Returns the value formerly found at i, paired with an array in which the value at i has been replaced with v.

                                                            Examples:

                                                            • #["spinach", "broccoli", "carrot"].swapAt! 1 "pepper" = (#["spinach", "pepper", "carrot"], "broccoli")
                                                            • #["spinach", "broccoli", "carrot"].swapAt! 2 "pepper" = (#["spinach", "broccoli", "pepper"], "carrot")
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def Array.shrink {α : Type u} (xs : Array α) (n : Nat) :

                                                              Returns the first n elements of an array. The resulting array is produced by repeatedly calling Array.pop. If n is greater than the size of the array, it is returned unmodified.

                                                              If the reference to the array is unique, then this function uses in-place modification.

                                                              Examples:

                                                              • #[0, 1, 2, 3, 4].shrink 2 = #[0, 1]
                                                              • #[0, 1, 2, 3, 4].shrink 0 = #[]
                                                              • #[0, 1, 2, 3, 4].shrink 10 = #[0, 1, 2, 3, 4]
                                                              Equations
                                                              Instances For
                                                                def Array.shrink.loop {α : Type u} :
                                                                NatArray αArray α
                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  abbrev Array.take {α : Type u} (xs : Array α) (i : Nat) :

                                                                  Returns a new array that contains the first i elements of xs. If xs has fewer than i elements, the new array contains all the elements of xs.

                                                                  The returned array is always a new array, even if it contains the same elements as the input array.

                                                                  Examples:

                                                                  • #["red", "green", "blue"].take 1 = #["red"]
                                                                  • #["red", "green", "blue"].take 2 = #["red", "green"]
                                                                  • #["red", "green", "blue"].take 5 = #["red", "green", "blue"]
                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem Array.take_eq_extract {α : Type u} {xs : Array α} {i : Nat} :
                                                                    xs.take i = xs.extract 0 i
                                                                    @[reducible, inline]
                                                                    abbrev Array.drop {α : Type u} (xs : Array α) (i : Nat) :

                                                                    Removes the first i elements of xs. If xs has fewer than i elements, the new array is empty.

                                                                    The returned array is always a new array, even if it contains the same elements as the input array.

                                                                    Examples:

                                                                    • #["red", "green", "blue"].drop 1 = #["green", "blue"]
                                                                    • #["red", "green", "blue"].drop 2 = #["blue"]
                                                                    • #["red", "green", "blue"].drop 5 = #[]
                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Array.drop_eq_extract {α : Type u} {xs : Array α} {i : Nat} :
                                                                      xs.drop i = xs.extract i
                                                                      @[inline]
                                                                      unsafe def Array.modifyMUnsafe {α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : Nat) (f : αm α) :
                                                                      m (Array α)
                                                                      Equations
                                                                      Instances For
                                                                        @[implemented_by Array.modifyMUnsafe]
                                                                        def Array.modifyM {α : Type u} {m : Type u → Type u_1} [Monad m] (xs : Array α) (i : Nat) (f : αm α) :
                                                                        m (Array α)

                                                                        Replaces the element at the given index, if it exists, with the result of applying the monadic function f to it. If the index is invalid, the array is returned unmodified and f is not called.

                                                                        Examples:

                                                                        #eval #[1, 2, 3, 4].modifyM 2 fun x => do
                                                                          IO.println s!"It was {x}"
                                                                          return x * 10
                                                                        
                                                                        It was 3
                                                                        
                                                                        #[1, 2, 30, 4]
                                                                        
                                                                        #eval #[1, 2, 3, 4].modifyM 6 fun x => do
                                                                          IO.println s!"It was {x}"
                                                                          return x * 10
                                                                        
                                                                        #[1, 2, 3, 4]
                                                                        
                                                                        Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def Array.modify {α : Type u} (xs : Array α) (i : Nat) (f : αα) :

                                                                          Replaces the element at the given index, if it exists, with the result of applying f to it. If the index is invalid, the array is returned unmodified.

                                                                          Examples:

                                                                          • #[1, 2, 3].modify 0 (· * 10) = #[10, 2, 3]
                                                                          • #[1, 2, 3].modify 2 (· * 10) = #[1, 2, 30]
                                                                          • #[1, 2, 3].modify 3 (· * 10) = #[1, 2, 3]
                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            def Array.modifyOp {α : Type u} (xs : Array α) (idx : Nat) (f : αα) :

                                                                            Replaces the element at the given index, if it exists, with the result of applying f to it. If the index is invalid, the array is returned unmodified.

                                                                            Examples:

                                                                            • #[1, 2, 3].modifyOp 0 (· * 10) = #[10, 2, 3]
                                                                            • #[1, 2, 3].modifyOp 2 (· * 10) = #[1, 2, 30]
                                                                            • #[1, 2, 3].modifyOp 3 (· * 10) = #[1, 2, 3]
                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              unsafe def Array.forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a asβ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.forIn'Unsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (a : α) → a asβm (ForInStep β)) (sz i : USize) (b : β) :
                                                                                m β
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[implemented_by Array.forIn'Unsafe]
                                                                                  def Array.forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a asβ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 : (a : α) → a asβm (ForInStep β)) (i : Nat) (h : i as.size) (b : β) :
                                                                                    m β
                                                                                    Equations
                                                                                    Instances For
                                                                                      instance Array.instForIn'InferInstanceMembership {α : Type u} {m : Type u_1 → Type u_2} :
                                                                                      Equations
                                                                                      @[simp]
                                                                                      theorem Array.forIn'_eq_forIn' {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] :
                                                                                      @[inline]
                                                                                      unsafe def Array.foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : βαm β) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :
                                                                                      m β

                                                                                      See comment at forIn'Unsafe

                                                                                      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 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 : Nat := 0) (stop : Nat := as.size) :
                                                                                          m β

                                                                                          Folds a monadic function over a list from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

                                                                                          The optional parameters start and stop control the region of the array to be folded. Folding proceeds from start (inclusive) to stop (exclusive), so no folding occurs unless start < stop. By default, the entire array is folded.

                                                                                          Examples:

                                                                                          example [Monad m] (f : α → β → m α) :
                                                                                              Array.foldlM (m := m) f x₀ #[a, b, c] = (do
                                                                                                let x₁ ← f x₀ a
                                                                                                let x₂ ← f x₁ b
                                                                                                let x₃ ← f x₂ c
                                                                                                pure x₃)
                                                                                            := by rfl
                                                                                          
                                                                                          example [Monad m] (f : α → β → m α) :
                                                                                              Array.foldlM (m := m) f x₀ #[a, b, c] (start := 1) = (do
                                                                                                let x₁ ← f x₀ b
                                                                                                let x₂ ← f x₁ c
                                                                                                pure x₂)
                                                                                            := by rfl
                                                                                          
                                                                                          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 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 : Nat := as.size) (stop : Nat := 0) :
                                                                                              m β

                                                                                              See comment at forIn'Unsafe

                                                                                              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 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 : Nat := as.size) (stop : Nat := 0) :
                                                                                                  m β

                                                                                                  Folds a monadic function over an array from the right, accumulating a value starting with init. The accumulated value is combined with the each element of the list in reverse order, using f.

                                                                                                  The optional parameters start and stop control the region of the array to be folded. Folding proceeds from start (exclusive) to stop (inclusive), so no folding occurs unless start > stop. By default, the entire array is folded.

                                                                                                  Examples:

                                                                                                  example [Monad m] (f : α → β → m β) :
                                                                                                    Array.foldrM (m := m) f x₀ #[a, b, c] = (do
                                                                                                      let x₁ ← f c x₀
                                                                                                      let x₂ ← f b x₁
                                                                                                      let x₃ ← f a x₂
                                                                                                      pure x₃)
                                                                                                    := by rfl
                                                                                                  
                                                                                                  example [Monad m] (f : α → β → m β) :
                                                                                                    Array.foldrM (m := m) f x₀ #[a, b, c] (start := 2) = (do
                                                                                                      let x₁ ← f b x₀
                                                                                                      let x₂ ← f a x₁
                                                                                                      pure x₂)
                                                                                                    := by rfl
                                                                                                  
                                                                                                  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 : 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 forIn'Unsafe

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[specialize #[]]
                                                                                                        unsafe def Array.mapMUnsafe.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm β) (sz i : USize) (bs : 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 β)

                                                                                                          Applies the monadic action f to every element in the array, left-to-right, and returns the array of results.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def Array.mapM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm β) (as : Array α) (i : Nat) (bs : Array β) :
                                                                                                            m (Array β)
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[reducible, inline, deprecated Array.mapM (since := "2024-11-11")]
                                                                                                              abbrev Array.sequenceMap {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] (f : αm β) (as : Array α) :
                                                                                                              m (Array β)
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                def Array.mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (i : Nat) → αi < as.sizem β) :
                                                                                                                m (Array β)

                                                                                                                Applies the monadic action f to every element in the array, along with the element's index and a proof that the index is in bounds, from left to right. Returns the array of results.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[specialize #[]]
                                                                                                                  def Array.mapFinIdxM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : (i : Nat) → αi < as.sizem β) (i j : Nat) (inv : i + j = as.size) (bs : Array β) :
                                                                                                                  m (Array β)
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def Array.mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Natαm β) (as : Array α) :
                                                                                                                    m (Array β)

                                                                                                                    Applies the monadic action f to every element in the array, along with the element's index, from left to right. Returns the array of results.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def Array.firstM {β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : αm β) (as : Array α) :
                                                                                                                      m β

                                                                                                                      Maps f over the array and collects the results with <|>. The result for the end of the array is failure.

                                                                                                                      Examples:

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[irreducible]
                                                                                                                        def Array.firstM.go {β : Type v} {α : Type u} {m : Type v → Type w} [Alternative m] (f : αm β) (as : Array α) (i : Nat) :
                                                                                                                        m β
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          def Array.findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm (Option β)) (as : Array α) :
                                                                                                                          m (Option β)

                                                                                                                          Returns the first non-none result of applying the monadic function f to each element of the array, in order. Returns none if f returns none for all elements.

                                                                                                                          Example:

                                                                                                                          #eval #[7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
                                                                                                                            if i < 5 then
                                                                                                                              return some (i * 10)
                                                                                                                            if i ≤ 6 then
                                                                                                                              IO.println s!"Almost! {i}"
                                                                                                                            return none
                                                                                                                          
                                                                                                                          Almost! 6
                                                                                                                          Almost! 5
                                                                                                                          
                                                                                                                          some 10
                                                                                                                          
                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            def Array.findM? {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) (as : Array α) :
                                                                                                                            m (Option α)

                                                                                                                            Returns the first element of the array for which the monadic predicate p returns true, or none if no such element is found. Elements of the array are checked in order.

                                                                                                                            The monad m is restricted to Type → Type to avoid needing to use ULift Bool in p's type.

                                                                                                                            Example:

                                                                                                                            #eval #[7, 6, 5, 8, 1, 2, 6].findM? fun i => do
                                                                                                                              if i < 5 then
                                                                                                                                return true
                                                                                                                              if i ≤ 6 then
                                                                                                                                IO.println s!"Almost! {i}"
                                                                                                                              return false
                                                                                                                            
                                                                                                                            Almost! 6
                                                                                                                            Almost! 5
                                                                                                                            
                                                                                                                            some 1
                                                                                                                            
                                                                                                                            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] (p : αm Bool) (as : Array α) :

                                                                                                                              Finds the index of the first element of an array for which the monadic predicate p returns true. Elements are examined in order from left to right, and the search is terminated when an element that satisfies p is found. If no such element exists in the array, then none is returned.

                                                                                                                              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 : Nat := 0) (stop : 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 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 : Nat := 0) (stop : Nat := as.size) :

                                                                                                                                    Returns true if the monadic predicate p returns true for any element of as.

                                                                                                                                    Short-circuits upon encountering the first true. The elements in as are examined in order from left to right.

                                                                                                                                    The optional parameters start and stop control the region of the array to be checked. Only the elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the entire array is checked.

                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      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 : Nat := 0) (stop : Nat := as.size) :

                                                                                                                                        Returns true if the monadic predicate p returns true for every element of as.

                                                                                                                                        Short-circuits upon encountering the first false. The elements in as are examined in order from left to right.

                                                                                                                                        The optional parameters start and stop control the region of the array to be checked. Only the elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the entire array is checked.

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline]
                                                                                                                                          def Array.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm (Option β)) (as : Array α) :
                                                                                                                                          m (Option β)

                                                                                                                                          Returns the first non-none result of applying the monadic function f to each element of the array in reverse order, from right to left. Once a non-none result is found, no further elements are checked. Returns none if f returns none for all elements of the array.

                                                                                                                                          Examples:

                                                                                                                                          #eval #[1, 2, 0, -4, 1].findSomeRevM? (m := Except String) fun x => do
                                                                                                                                            if x = 0 then throw "Zero!"
                                                                                                                                            else if x < 0 then return (some x)
                                                                                                                                            else return none
                                                                                                                                          
                                                                                                                                          Except.ok (some (-4))
                                                                                                                                          
                                                                                                                                          #eval #[1, 2, 0, 4, 1].findSomeRevM? (m := Except String) fun x => do
                                                                                                                                            if x = 0 then throw "Zero!"
                                                                                                                                            else if x < 0 then return (some x)
                                                                                                                                            else return none
                                                                                                                                          
                                                                                                                                          Except.error "Zero!"
                                                                                                                                          
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            @[specialize #[]]
                                                                                                                                            def Array.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm (Option β)) (as : Array α) (i : Nat) :
                                                                                                                                            i as.sizem (Option β)
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[inline]
                                                                                                                                              def Array.findRevM? {α : Type} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) :
                                                                                                                                              m (Option α)

                                                                                                                                              Returns the last element of the array for which the monadic predicate p returns true, or none if no such element is found. Elements of the array are checked in reverse, from right to left..

                                                                                                                                              The monad m is restricted to Type → Type to avoid needing to use ULift Bool in p's type.

                                                                                                                                              Example:

                                                                                                                                              #eval #[7, 5, 8, 1, 2, 6, 5, 8].findRevM? fun i => do
                                                                                                                                                if i < 5 then
                                                                                                                                                  return true
                                                                                                                                                if i ≤ 6 then
                                                                                                                                                  IO.println s!"Almost! {i}"
                                                                                                                                                return false
                                                                                                                                              
                                                                                                                                              Almost! 5
                                                                                                                                              Almost! 6
                                                                                                                                              
                                                                                                                                              some 2
                                                                                                                                              
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                def Array.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

                                                                                                                                                Applies the monadic action f to each element of an array, in order.

                                                                                                                                                The optional parameters start and stop control the region of the array to which f should be applied. Iteration proceeds from start (inclusive) to stop (exclusive), so f is not invoked unless start < stop. By default, the entire array is used.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  instance Array.instForM {α : Type u} {m : Type u_1 → Type u_2} :
                                                                                                                                                  ForM m (Array α) α
                                                                                                                                                  Equations
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem Array.forM_eq_forM {α : Type u} {m : Type u_1 → Type u_2} {as : Array α} [Monad m] {f : αm PUnit} :
                                                                                                                                                  Array.forM f as = forM as f
                                                                                                                                                  @[inline]
                                                                                                                                                  def Array.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :

                                                                                                                                                  Applies the monadic action f to each element of an array from right to left, in reverse order.

                                                                                                                                                  The optional parameters start and stop control the region of the array to which f should be applied. Iteration proceeds from start (exclusive) to stop (inclusive), so no f is not invoked unless start > stop. By default, the entire array is used.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[inline]
                                                                                                                                                    def Array.foldl {α : Type u} {β : Type v} (f : βαβ) (init : β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :
                                                                                                                                                    β

                                                                                                                                                    Folds a function over an array from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the array in order, using f.

                                                                                                                                                    The optional parameters start and stop control the region of the array to be folded. Folding proceeds from start (inclusive) to stop (exclusive), so no folding occurs unless start < stop. By default, the entire array is used.

                                                                                                                                                    Examples:

                                                                                                                                                    • #[a, b, c].foldl f z = f (f (f z a) b) c
                                                                                                                                                    • #[1, 2, 3].foldl (· ++ toString ·) "" = "123"
                                                                                                                                                    • #[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      def Array.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :
                                                                                                                                                      β

                                                                                                                                                      Folds a function over an array from the right, accumulating a value starting with init. The accumulated value is combined with the each element of the array in reverse order, using f.

                                                                                                                                                      The optional parameters start and stop control the region of the array to be folded. Folding proceeds from start (exclusive) to stop (inclusive), so no folding occurs unless start > stop. By default, the entire array is used.

                                                                                                                                                      Examples:

                                                                                                                                                      • #[a, b, c].foldr f init = f a (f b (f c init))
                                                                                                                                                      • #[1, 2, 3].foldr (toString · ++ ·) "" = "123"
                                                                                                                                                      • #[1, 2, 3].foldr (s!"({·} {·})") "!" = "(1 (2 (3 !)))"
                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        def Array.sum {α : Type u_1} [Add α] [Zero α] :
                                                                                                                                                        Array αα

                                                                                                                                                        Computes the sum of the elements of an array.

                                                                                                                                                        Examples:

                                                                                                                                                        • #[a, b, c].sum = a + (b + (c + 0))
                                                                                                                                                        • #[1, 2, 5].sum = 8
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def Array.countP {α : Type u} (p : αBool) (as : Array α) :

                                                                                                                                                          Counts the number of elements in the array as that satisfy the Boolean predicate p.

                                                                                                                                                          Examples:

                                                                                                                                                          • #[1, 2, 3, 4, 5].countP (· % 2 == 0) = 2
                                                                                                                                                          • #[1, 2, 3, 4, 5].countP (· < 5) = 4
                                                                                                                                                          • #[1, 2, 3, 4, 5].countP (· > 5) = 0
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            def Array.count {α : Type u} [BEq α] (a : α) (as : Array α) :

                                                                                                                                                            Counts the number of times an element occurs in an array.

                                                                                                                                                            Examples:

                                                                                                                                                            • #[1, 1, 2, 3, 5].count 1 = 2
                                                                                                                                                            • #[1, 1, 2, 3, 5].count 5 = 1
                                                                                                                                                            • #[1, 1, 2, 3, 5].count 4 = 0
                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              def Array.map {α : Type u} {β : Type v} (f : αβ) (as : Array α) :

                                                                                                                                                              Applies a function to each element of the array, returning the resulting array of values.

                                                                                                                                                              Examples:

                                                                                                                                                              • #[a, b, c].map f = #[f a, f b, f c]
                                                                                                                                                              • #[].map Nat.succ = #[]
                                                                                                                                                              • #["one", "two", "three"].map (·.length) = #[3, 3, 5]
                                                                                                                                                              • #["one", "two", "three"].map (·.reverse) = #["eno", "owt", "eerht"]
                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                Equations
                                                                                                                                                                @[inline]
                                                                                                                                                                def Array.mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → αi < as.sizeβ) :

                                                                                                                                                                Applies a function to each element of the array along with the index at which that element is found, returning the array of results. In addition to the index, the function is also provided with a proof that the index is valid.

                                                                                                                                                                Array.mapIdx is a variant that does not provide the function with evidence that the index is valid.

                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  def Array.mapIdx {α : Type u} {β : Type v} (f : Natαβ) (as : Array α) :

                                                                                                                                                                  Applies a function to each element of the array along with the index at which that element is found, returning the array of results.

                                                                                                                                                                  Array.mapFinIdx is a variant that additionally provides the function with a proof that the index is valid.

                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    def Array.zipIdx {α : Type u} (xs : Array α) (start : Nat := 0) :
                                                                                                                                                                    Array (α × Nat)

                                                                                                                                                                    Pairs each element of an array with its index, optionally starting from an index other than 0.

                                                                                                                                                                    Examples:

                                                                                                                                                                    • #[a, b, c].zipIdx = #[(a, 0), (b, 1), (c, 2)]
                                                                                                                                                                    • #[a, b, c].zipIdx 5 = #[(a, 5), (b, 6), (c, 7)]
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[reducible, inline, deprecated Array.zipIdx (since := "2025-01-21")]
                                                                                                                                                                      abbrev Array.zipWithIndex {α : Type u_1} (xs : Array α) (start : Nat := 0) :
                                                                                                                                                                      Array (α × Nat)
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]
                                                                                                                                                                        def Array.find? {α : Type u} (p : αBool) (as : Array α) :

                                                                                                                                                                        Returns the first element of the array for which the predicate p returns true, or none if no such element is found.

                                                                                                                                                                        Examples:

                                                                                                                                                                        • #[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1
                                                                                                                                                                        • #[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none
                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          def Array.findSome? {α : Type u} {β : Type v} (f : αOption β) (as : Array α) :

                                                                                                                                                                          Returns the first non-none result of applying the function f to each element of the array, in order. Returns none if f returns none for all elements.

                                                                                                                                                                          Example:

                                                                                                                                                                          #eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i =>
                                                                                                                                                                            if i < 5 then
                                                                                                                                                                              some (i * 10)
                                                                                                                                                                            else
                                                                                                                                                                              none
                                                                                                                                                                          
                                                                                                                                                                          some 10
                                                                                                                                                                          
                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            def Array.findSome! {α : Type u} {β : Type v} [Inhabited β] (f : αOption β) (xs : Array α) :
                                                                                                                                                                            β

                                                                                                                                                                            Returns the first non-none result of applying the function f to each element of the array, in order. Panics if f returns none for all elements.

                                                                                                                                                                            Example:

                                                                                                                                                                            #eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i =>
                                                                                                                                                                              if i < 5 then
                                                                                                                                                                                some (i * 10)
                                                                                                                                                                              else
                                                                                                                                                                                none
                                                                                                                                                                            
                                                                                                                                                                            some 10
                                                                                                                                                                            
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline]
                                                                                                                                                                              def Array.findSomeRev? {α : Type u} {β : Type v} (f : αOption β) (as : Array α) :

                                                                                                                                                                              Returns the first non-none result of applying f to each element of the array in reverse order, from right to left. Returns none if f returns none for all elements of the array.

                                                                                                                                                                              Examples:

                                                                                                                                                                              • #[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10
                                                                                                                                                                              • #[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[inline]
                                                                                                                                                                                def Array.findRev? {α : Type} (p : αBool) (as : Array α) :

                                                                                                                                                                                Returns the last element of the array for which the predicate p returns true, or none if no such element is found.

                                                                                                                                                                                Examples:

                                                                                                                                                                                • #[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2
                                                                                                                                                                                • #[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]
                                                                                                                                                                                  def Array.findIdx? {α : Type u} (p : αBool) (as : Array α) :

                                                                                                                                                                                  Returns the index of the first element for which p returns true, or none if there is no such element.

                                                                                                                                                                                  Examples:

                                                                                                                                                                                  • #[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4
                                                                                                                                                                                  • #[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none
                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    def Array.findIdx?.loop {α : Type u} (p : αBool) (as : Array α) (j : Nat) :
                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      def Array.findFinIdx? {α : Type u} (p : αBool) (as : Array α) :

                                                                                                                                                                                      Returns the index of the first element for which p returns true, or none if there is no such element. The index is returned as a Fin, which guarantees that it is in bounds.

                                                                                                                                                                                      Examples:

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        def Array.findFinIdx?.loop {α : Type u} (p : αBool) (as : Array α) (j : Nat) :
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[irreducible]
                                                                                                                                                                                          theorem Array.findIdx?_loop_eq_map_findFinIdx?_loop_val {α : Type u} {xs : Array α} {p : αBool} {j : Nat} :
                                                                                                                                                                                          findIdx?.loop p xs j = Option.map (fun (x : Fin xs.size) => x) (findFinIdx?.loop p xs j)
                                                                                                                                                                                          theorem Array.findIdx?_eq_map_findFinIdx?_val {α : Type u} {xs : Array α} {p : αBool} :
                                                                                                                                                                                          findIdx? p xs = Option.map (fun (x : Fin xs.size) => x) (findFinIdx? p xs)
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          def Array.findIdx {α : Type u} (p : αBool) (as : Array α) :

                                                                                                                                                                                          Returns the index of the first element for which p returns true, or the size of the array if there is no such element.

                                                                                                                                                                                          Examples:

                                                                                                                                                                                          • #[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = 4
                                                                                                                                                                                          • #[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = 7
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            def Array.idxOfAux {α : Type u} [BEq α] (xs : Array α) (v : α) (i : Nat) :
                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[reducible, inline, deprecated Array.idxOfAux (since := "2025-01-29")]
                                                                                                                                                                                              abbrev Array.indexOfAux {α : Type u_1} [BEq α] (xs : Array α) (v : α) (i : Nat) :
                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                def Array.finIdxOf? {α : Type u} [BEq α] (xs : Array α) (v : α) :

                                                                                                                                                                                                Returns the index of the first element equal to a, or the size of the array if no element is equal to a. The index is returned as a Fin, which guarantees that it is in bounds.

                                                                                                                                                                                                Examples:

                                                                                                                                                                                                • #["carrot", "potato", "broccoli"].finIdxOf? "carrot" = some 0
                                                                                                                                                                                                • #["carrot", "potato", "broccoli"].finIdxOf? "broccoli" = some 2
                                                                                                                                                                                                • #["carrot", "potato", "broccoli"].finIdxOf? "tomato" = none
                                                                                                                                                                                                • #["carrot", "potato", "broccoli"].finIdxOf? "anything else" = none
                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[reducible, inline, deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")]
                                                                                                                                                                                                  abbrev Array.indexOf? {α : Type u_1} [BEq α] (xs : Array α) (v : α) :
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    def Array.idxOf {α : Type u} [BEq α] (a : α) :
                                                                                                                                                                                                    Array αNat

                                                                                                                                                                                                    Returns the index of the first element equal to a, or the size of the array if no element is equal to a.

                                                                                                                                                                                                    Examples:

                                                                                                                                                                                                    • #["carrot", "potato", "broccoli"].idxOf "carrot" = 0
                                                                                                                                                                                                    • #["carrot", "potato", "broccoli"].idxOf "broccoli" = 2
                                                                                                                                                                                                    • #["carrot", "potato", "broccoli"].idxOf "tomato" = 3
                                                                                                                                                                                                    • #["carrot", "potato", "broccoli"].idxOf "anything else" = 3
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      def Array.idxOf? {α : Type u} [BEq α] (xs : Array α) (v : α) :

                                                                                                                                                                                                      Returns the index of the first element equal to a, or none if no element is equal to a.

                                                                                                                                                                                                      Examples:

                                                                                                                                                                                                      • #["carrot", "potato", "broccoli"].idxOf? "carrot" = some 0
                                                                                                                                                                                                      • #["carrot", "potato", "broccoli"].idxOf? "broccoli" = some 2
                                                                                                                                                                                                      • #["carrot", "potato", "broccoli"].idxOf? "tomato" = none
                                                                                                                                                                                                      • #["carrot", "potato", "broccoli"].idxOf? "anything else" = none
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[deprecated Array.idxOf? (since := "2024-11-20")]
                                                                                                                                                                                                        def Array.getIdx? {α : Type u} [BEq α] (xs : Array α) (v : α) :
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                          def Array.any {α : Type u} (as : Array α) (p : αBool) (start : Nat := 0) (stop : Nat := as.size) :

                                                                                                                                                                                                          Returns true if p returns true for any element of as.

                                                                                                                                                                                                          Short-circuits upon encountering the first true.

                                                                                                                                                                                                          The optional parameters start and stop control the region of the array to be checked. Only the elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the entire array is checked.

                                                                                                                                                                                                          Examples:

                                                                                                                                                                                                          • #[2, 4, 6].any (· % 2 = 0) = true
                                                                                                                                                                                                          • #[2, 4, 6].any (· % 2 = 1) = false
                                                                                                                                                                                                          • #[2, 4, 5, 6].any (· % 2 = 0) = true
                                                                                                                                                                                                          • #[2, 4, 5, 6].any (· % 2 = 1) = true
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                            def Array.all {α : Type u} (as : Array α) (p : αBool) (start : Nat := 0) (stop : Nat := as.size) :

                                                                                                                                                                                                            Returns true if p returns true for every element of as.

                                                                                                                                                                                                            Short-circuits upon encountering the first false.

                                                                                                                                                                                                            The optional parameters start and stop control the region of the array to be checked. Only the elements with indices from start (inclusive) to stop (exclusive) are checked. By default, the entire array is checked.

                                                                                                                                                                                                            Examples:

                                                                                                                                                                                                            • #[a, b, c].all p = (p a && (p b && p c))
                                                                                                                                                                                                            • #[2, 4, 6].all (· % 2 = 0) = true
                                                                                                                                                                                                            • #[2, 4, 5, 6].all (· % 2 = 0) = false
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def Array.contains {α : Type u} [BEq α] (as : Array α) (a : α) :

                                                                                                                                                                                                              Checks whether a is an element of as, using == to compare elements.

                                                                                                                                                                                                              Array.elem is a synonym that takes the element before the array.

                                                                                                                                                                                                              Examples:

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                def Array.elem {α : Type u} [BEq α] (a : α) (as : Array α) :

                                                                                                                                                                                                                Checks whether a is an element of as, using == to compare elements.

                                                                                                                                                                                                                Array.contains is a synonym that takes the array before the element.

                                                                                                                                                                                                                For verification purposes, Array.elem is simplified to Array.contains.

                                                                                                                                                                                                                Example:

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[export lean_array_to_list_impl]
                                                                                                                                                                                                                  def Array.toListImpl {α : 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 to a list. The elements of the array are at the beginning of the resulting list.

                                                                                                                                                                                                                    Equivalent to as.toList ++ l.

                                                                                                                                                                                                                    Examples:

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      def Array.append {α : Type u} (as bs : Array α) :

                                                                                                                                                                                                                      Appends two arrays. Normally used via the ++ operator.

                                                                                                                                                                                                                      Appending arrays takes time proportional to the length of the second array.

                                                                                                                                                                                                                      Examples:

                                                                                                                                                                                                                      • #[1, 2, 3] ++ #[4, 5] = #[1, 2, 3, 4, 5].
                                                                                                                                                                                                                      • #[] ++ #[4, 5] = #[4, 5].
                                                                                                                                                                                                                      • #[1, 2, 3] ++ #[] = #[1, 2, 3].
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        instance Array.instAppend {α : Type u} :
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        def Array.appendList {α : Type u} (as : Array α) (bs : List α) :

                                                                                                                                                                                                                        Appends an array and a list.

                                                                                                                                                                                                                        Takes time proportional to the length of the list..

                                                                                                                                                                                                                        Examples:

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          instance Array.instHAppendList {α : Type u} :
                                                                                                                                                                                                                          HAppend (Array α) (List α) (Array α)
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                          def Array.flatMapM {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : αm (Array β)) (as : Array α) :
                                                                                                                                                                                                                          m (Array β)

                                                                                                                                                                                                                          Applies a monadic function that returns an array to each element of an array, from left to right. The resulting arrays are appended.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            @[reducible, inline, deprecated Array.flatMapM (since := "2024-10-16")]
                                                                                                                                                                                                                            abbrev Array.concatMapM {α : Type u_1} {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : αm (Array β)) (as : Array α) :
                                                                                                                                                                                                                            m (Array β)
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                              def Array.flatMap {α : Type u} {β : Type u_1} (f : αArray β) (as : Array α) :

                                                                                                                                                                                                                              Applies a function that returns an array to each element of an array. The resulting arrays are appended.

                                                                                                                                                                                                                              Examples:

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                @[reducible, inline, deprecated Array.flatMap (since := "2024-10-16")]
                                                                                                                                                                                                                                abbrev Array.concatMap {α : Type u_1} {β : Type u_2} (f : αArray β) (as : Array α) :
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                  def Array.flatten {α : Type u} (xss : Array (Array α)) :

                                                                                                                                                                                                                                  Appends the contents of array of arrays into a single array. The resulting array contains the same elements as the nested arrays in the same order.

                                                                                                                                                                                                                                  Examples:

                                                                                                                                                                                                                                  • #[#[5], #[4], #[3, 2]].flatten = #[5, 4, 3, 2]
                                                                                                                                                                                                                                  • #[#[0, 1], #[], #[2], #[1, 0, 1]].flatten = #[0, 1, 2, 1, 0, 1]
                                                                                                                                                                                                                                  • (#[] : Array Nat).flatten = #[]
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    def Array.reverse {α : Type u} (as : Array α) :

                                                                                                                                                                                                                                    Reverses an array by repeatedly swapping elements.

                                                                                                                                                                                                                                    The original array is modified in place if there are no other references to it.

                                                                                                                                                                                                                                    Examples:

                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      theorem Array.reverse.termination {i j : Nat} (h : i < j) :
                                                                                                                                                                                                                                      j - 1 - (i + 1) < j - i
                                                                                                                                                                                                                                      @[irreducible]
                                                                                                                                                                                                                                      def Array.reverse.loop {α : Type u} (as : Array α) (i : Nat) (j : Fin as.size) :
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                        def Array.filter {α : Type u} (p : αBool) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

                                                                                                                                                                                                                                        Returns the array of elements in as for which p returns true.

                                                                                                                                                                                                                                        Only elements from start (inclusive) to stop (exclusive) are considered. Elements outside that range are discarded. By default, the entire array is considered.

                                                                                                                                                                                                                                        Examples:

                                                                                                                                                                                                                                        • #[1, 2, 5, 2, 7, 7].filter (· > 2) = #[5, 7, 7]
                                                                                                                                                                                                                                        • #[1, 2, 5, 2, 7, 7].filter (fun _ => false) = #[]
                                                                                                                                                                                                                                        • #[1, 2, 5, 2, 7, 7].filter (fun _ => true) = #[1, 2, 5, 2, 7, 7]
                                                                                                                                                                                                                                        • #[1, 2, 5, 2, 7, 7].filter (· > 2) (start := 3) = #[7, 7]
                                                                                                                                                                                                                                        • #[1, 2, 5, 2, 7, 7].filter (fun _ => true) (start := 3) = #[2, 7, 7]
                                                                                                                                                                                                                                        • #[1, 2, 5, 2, 7, 7].filter (fun _ => true) (stop := 3) = #[1, 2, 5]
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                          def Array.filterM {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :
                                                                                                                                                                                                                                          m (Array α)

                                                                                                                                                                                                                                          Applies the monadic predicate p to every element in the array, in order from left to right, and returns the array of elements for which p returns true.

                                                                                                                                                                                                                                          Only elements from start (inclusive) to stop (exclusive) are considered. Elements outside that range are discarded. By default, the entire array is checked.

                                                                                                                                                                                                                                          Example:

                                                                                                                                                                                                                                          #eval #[1, 2, 5, 2, 7, 7].filterM fun x => do
                                                                                                                                                                                                                                            IO.println s!"Checking {x}"
                                                                                                                                                                                                                                            return x < 3
                                                                                                                                                                                                                                          
                                                                                                                                                                                                                                          Checking 1
                                                                                                                                                                                                                                          Checking 2
                                                                                                                                                                                                                                          Checking 5
                                                                                                                                                                                                                                          Checking 2
                                                                                                                                                                                                                                          Checking 7
                                                                                                                                                                                                                                          Checking 7
                                                                                                                                                                                                                                          
                                                                                                                                                                                                                                          #[1, 2, 2]
                                                                                                                                                                                                                                          
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                            def Array.filterRevM {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) (as : Array α) (start : Nat := as.size) (stop : Nat := 0) :
                                                                                                                                                                                                                                            m (Array α)

                                                                                                                                                                                                                                            Applies the monadic predicate p on every element in the array in reverse order, from right to left, and returns those elements for which p returns true. The elements of the returned list are in the same order as in the input list.

                                                                                                                                                                                                                                            Only elements from start (exclusive) to stop (inclusive) are considered. Elements outside that range are discarded. Because the array is examined in reverse order, elements are only examined when start > stop. By default, the entire array is considered.

                                                                                                                                                                                                                                            Example:

                                                                                                                                                                                                                                            #eval #[1, 2, 5, 2, 7, 7].filterRevM fun x => do
                                                                                                                                                                                                                                              IO.println s!"Checking {x}"
                                                                                                                                                                                                                                              return x < 3
                                                                                                                                                                                                                                            
                                                                                                                                                                                                                                            Checking 7
                                                                                                                                                                                                                                            Checking 7
                                                                                                                                                                                                                                            Checking 2
                                                                                                                                                                                                                                            Checking 5
                                                                                                                                                                                                                                            Checking 2
                                                                                                                                                                                                                                            Checking 1
                                                                                                                                                                                                                                            
                                                                                                                                                                                                                                            #[1, 2, 2]
                                                                                                                                                                                                                                            
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              @[specialize #[]]
                                                                                                                                                                                                                                              def Array.filterMapM {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : αm (Option β)) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :
                                                                                                                                                                                                                                              m (Array β)

                                                                                                                                                                                                                                              Applies a monadic function that returns an Option to each element of an array, collecting the non-none values.

                                                                                                                                                                                                                                              Only elements from start (inclusive) to stop (exclusive) are considered. Elements outside that range are discarded. By default, the entire array is considered.

                                                                                                                                                                                                                                              Example:

                                                                                                                                                                                                                                              #eval #[1, 2, 5, 2, 7, 7].filterMapM fun x => do
                                                                                                                                                                                                                                                IO.println s!"Examining {x}"
                                                                                                                                                                                                                                                if x > 2 then return some (2 * x)
                                                                                                                                                                                                                                                else return none
                                                                                                                                                                                                                                              
                                                                                                                                                                                                                                              Examining 1
                                                                                                                                                                                                                                              Examining 2
                                                                                                                                                                                                                                              Examining 5
                                                                                                                                                                                                                                              Examining 2
                                                                                                                                                                                                                                              Examining 7
                                                                                                                                                                                                                                              Examining 7
                                                                                                                                                                                                                                              
                                                                                                                                                                                                                                              #[10, 14, 14]
                                                                                                                                                                                                                                              
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                def Array.filterMap {α : Type u} {β : Type u_1} (f : αOption β) (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :

                                                                                                                                                                                                                                                Applies a function that returns an Option to each element of an array, collecting the non-none values.

                                                                                                                                                                                                                                                Example:

                                                                                                                                                                                                                                                #eval #[1, 2, 5, 2, 7, 7].filterMap fun x =>
                                                                                                                                                                                                                                                  if x > 2 then some (2 * x) else none
                                                                                                                                                                                                                                                
                                                                                                                                                                                                                                                #[10, 14, 14]
                                                                                                                                                                                                                                                
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  @[specialize #[]]
                                                                                                                                                                                                                                                  def Array.getMax? {α : Type u} (as : Array α) (lt : ααBool) :

                                                                                                                                                                                                                                                  Returns the largest element of the array, as determined by the comparison lt, or none if the array is empty.

                                                                                                                                                                                                                                                  Examples:

                                                                                                                                                                                                                                                  • (#[] : Array Nat).getMax? (· < ·) = none
                                                                                                                                                                                                                                                  • #["red", "green", "blue"].getMax? (·.length < ·.length) = some "green"
                                                                                                                                                                                                                                                  • #["red", "green", "blue"].getMax? (· < ·) = some "red"
                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                    def Array.partition {α : Type u} (p : αBool) (as : Array α) :
                                                                                                                                                                                                                                                    Array α × Array α

                                                                                                                                                                                                                                                    Returns a pair of arrays that together contain all the elements of as. The first array contains those elements for which p returns true, and the second contains those for which p returns false.

                                                                                                                                                                                                                                                    as.partition p is equivalent to (as.filter p, as.filter (not ∘ p)), but it is more efficient since it only has to do one pass over the array.

                                                                                                                                                                                                                                                    Examples:

                                                                                                                                                                                                                                                    • #[1, 2, 5, 2, 7, 7].partition (· > 2) = (#[5, 7, 7], #[1, 2, 2])
                                                                                                                                                                                                                                                    • #[1, 2, 5, 2, 7, 7].partition (fun _ => false) = (#[], #[1, 2, 5, 2, 7, 7])
                                                                                                                                                                                                                                                    • #[1, 2, 5, 2, 7, 7].partition (fun _ => true) = (#[1, 2, 5, 2, 7, 7], #[])
                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      def Array.popWhile {α : Type u} (p : αBool) (as : Array α) :

                                                                                                                                                                                                                                                      Removes all the elements that satisfy a predicate from the end of an array.

                                                                                                                                                                                                                                                      The longest contiguous sequence of elements that all satisfy the predicate is removed.

                                                                                                                                                                                                                                                      Examples:

                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        @[simp]
                                                                                                                                                                                                                                                        theorem Array.popWhile_empty {α : Type u} {p : αBool} :
                                                                                                                                                                                                                                                        def Array.takeWhile {α : Type u} (p : αBool) (as : Array α) :

                                                                                                                                                                                                                                                        Returns a new array that contains the longest prefix of elements that satisfy the predicate p from an array.

                                                                                                                                                                                                                                                        Examples:

                                                                                                                                                                                                                                                        • #[0, 1, 2, 3, 2, 1].takeWhile (· < 2) = #[0, 1]
                                                                                                                                                                                                                                                        • #[0, 1, 2, 3, 2, 1].takeWhile (· < 20) = #[0, 1, 2, 3, 2, 1]
                                                                                                                                                                                                                                                        • #[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          def Array.takeWhile.go {α : Type u} (p : αBool) (as : Array α) (i : Nat) (acc : Array α) :
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            def Array.eraseIdx {α : Type u} (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) :

                                                                                                                                                                                                                                                            Removes the element at a given index from an array without a run-time bounds check.

                                                                                                                                                                                                                                                            This function takes worst-case O(n) time because it back-shifts all elements at positions greater than i.

                                                                                                                                                                                                                                                            Examples:

                                                                                                                                                                                                                                                            • #["apple", "pear", "orange"].eraseIdx 0 = #["pear", "orange"]
                                                                                                                                                                                                                                                            • #["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]
                                                                                                                                                                                                                                                            • #["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              @[simp]
                                                                                                                                                                                                                                                              theorem Array.size_eraseIdx {α : Type u} {xs : Array α} (i : Nat) (h : i < xs.size) :
                                                                                                                                                                                                                                                              (xs.eraseIdx i h).size = xs.size - 1
                                                                                                                                                                                                                                                              def Array.eraseIdxIfInBounds {α : Type u} (xs : Array α) (i : Nat) :

                                                                                                                                                                                                                                                              Removes the element at a given index from an array. Does nothing if the index is out of bounds.

                                                                                                                                                                                                                                                              This function takes worst-case O(n) time because it back-shifts all elements at positions greater than i.

                                                                                                                                                                                                                                                              Examples:

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                def Array.eraseIdx! {α : Type u} (xs : Array α) (i : Nat) :

                                                                                                                                                                                                                                                                Removes the element at a given index from an array. Panics if the index is out of bounds.

                                                                                                                                                                                                                                                                This function takes worst-case O(n) time because it back-shifts all elements at positions greater than i.

                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  def Array.erase {α : Type u} [BEq α] (as : Array α) (a : α) :

                                                                                                                                                                                                                                                                  Removes the first occurrence of a specified element from an array, or does nothing if it is not present.

                                                                                                                                                                                                                                                                  This function takes worst-case O(n) time because it back-shifts all later elements.

                                                                                                                                                                                                                                                                  Examples:

                                                                                                                                                                                                                                                                  • #[1, 2, 3].erase 2 = #[1, 3]
                                                                                                                                                                                                                                                                  • #[1, 2, 3].erase 5 = #[1, 2, 3]
                                                                                                                                                                                                                                                                  • #[1, 2, 3, 2, 1].erase 2 = #[1, 3, 2, 1]
                                                                                                                                                                                                                                                                  • (#[] : List Nat).erase 2 = #[]
                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    def Array.eraseP {α : Type u} (as : Array α) (p : αBool) :

                                                                                                                                                                                                                                                                    Removes the first element that satisfies the predicate p. If no element satisfies p, the array is returned unmodified.

                                                                                                                                                                                                                                                                    This function takes worst-case O(n) time because it back-shifts all later elements.

                                                                                                                                                                                                                                                                    Examples:

                                                                                                                                                                                                                                                                    • #["red", "green", "", "blue"].eraseP (·.isEmpty) = #["red", "green", "blue"]
                                                                                                                                                                                                                                                                    • #["red", "green", "", "blue", ""].eraseP (·.isEmpty) = #["red", "green", "blue", ""]
                                                                                                                                                                                                                                                                    • #["red", "green", "blue"].eraseP (·.length % 2 == 0) = #["red", "green"]
                                                                                                                                                                                                                                                                    • #["red", "green", "blue"].eraseP (fun _ => true) = #["green", "blue"]
                                                                                                                                                                                                                                                                    • (#[] : Array String).eraseP (fun _ => true) = #[]
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                      def Array.insertIdx {α : Type u} (as : Array α) (i : Nat) (a : α) :

                                                                                                                                                                                                                                                                      Inserts an element into an array at the specified index. If the index is greater than the size of the array, then the array is returned unmodified.

                                                                                                                                                                                                                                                                      In other words, the new element is inserted into the array as after the first i elements of as.

                                                                                                                                                                                                                                                                      This function takes worst case O(n) time because it has to swap the inserted element into place.

                                                                                                                                                                                                                                                                      Examples:

                                                                                                                                                                                                                                                                      • #["tues", "thur", "sat"].insertIdx 1 "wed" = #["tues", "wed", "thur", "sat"]
                                                                                                                                                                                                                                                                      • #["tues", "thur", "sat"].insertIdx 2 "wed" = #["tues", "thur", "wed", "sat"]
                                                                                                                                                                                                                                                                      • #["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]
                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        def Array.insertIdx.loop {α : Type u} (i : Nat) (as : Array α) (j : Fin as.size) :
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          @[reducible, inline, deprecated Array.insertIdx (since := "2024-11-20")]
                                                                                                                                                                                                                                                                          abbrev Array.insertAt {α : Type u_1} (as : Array α) (i : Nat) (a : α) :
                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                            def Array.insertIdx! {α : Type u} (as : Array α) (i : Nat) (a : α) :

                                                                                                                                                                                                                                                                            Inserts an element into an array at the specified index. Panics if the index is greater than the size of the array.

                                                                                                                                                                                                                                                                            In other words, the new element is inserted into the array as after the first i elements of as.

                                                                                                                                                                                                                                                                            This function takes worst case O(n) time because it has to swap the inserted element into place. Array.insertIdx and Array.insertIdxIfInBounds are safer alternatives.

                                                                                                                                                                                                                                                                            Examples:

                                                                                                                                                                                                                                                                            • #["tues", "thur", "sat"].insertIdx! 1 "wed" = #["tues", "wed", "thur", "sat"]
                                                                                                                                                                                                                                                                            • #["tues", "thur", "sat"].insertIdx! 2 "wed" = #["tues", "thur", "wed", "sat"]
                                                                                                                                                                                                                                                                            • #["tues", "thur", "sat"].insertIdx! 3 "wed" = #["tues", "thur", "sat", "wed"]
                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              @[reducible, inline, deprecated Array.insertIdx! (since := "2024-11-20")]
                                                                                                                                                                                                                                                                              abbrev Array.insertAt! {α : Type u_1} (as : Array α) (i : Nat) (a : α) :
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                def Array.insertIdxIfInBounds {α : Type u} (as : Array α) (i : Nat) (a : α) :

                                                                                                                                                                                                                                                                                Inserts an element into an array at the specified index. The array is returned unmodified if the index is greater than the size of the array.

                                                                                                                                                                                                                                                                                In other words, the new element is inserted into the array as after the first i elements of as.

                                                                                                                                                                                                                                                                                This function takes worst case O(n) time because it has to swap the inserted element into place.

                                                                                                                                                                                                                                                                                Examples:

                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  def Array.isPrefixOfAux {α : Type u} [BEq α] (as bs : Array α) (hle : as.size bs.size) (i : Nat) :
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                    def Array.isPrefixOf {α : Type u} [BEq α] (as bs : Array α) :

                                                                                                                                                                                                                                                                                    Return true if as is a prefix of bs, or false otherwise.

                                                                                                                                                                                                                                                                                    Examples:

                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      @[specialize #[]]
                                                                                                                                                                                                                                                                                      def Array.zipWithAux {α : Type u} {β : Type u_1} {γ : Type u_2} (as : Array α) (bs : Array β) (f : αβγ) (i : Nat) (cs : Array γ) :
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                        def Array.zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (as : Array α) (bs : Array β) :

                                                                                                                                                                                                                                                                                        Applies a function to the corresponding elements of two arrays, stopping at the end of the shorter array.

                                                                                                                                                                                                                                                                                        Examples:

                                                                                                                                                                                                                                                                                        • #[1, 2].zipWith (· + ·) #[5, 6] = #[6, 8]
                                                                                                                                                                                                                                                                                        • #[1, 2, 3].zipWith (· + ·) #[5, 6, 10] = #[6, 8, 13]
                                                                                                                                                                                                                                                                                        • #[].zipWith (· + ·) #[5, 6] = #[]
                                                                                                                                                                                                                                                                                        • #[x₁, x₂, x₃].zipWith f #[y₁, y₂, y₃, y₄] = #[f x₁ y₁, f x₂ y₂, f x₃ y₃]
                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          def Array.zip {α : Type u} {β : Type u_1} (as : Array α) (bs : Array β) :
                                                                                                                                                                                                                                                                                          Array (α × β)

                                                                                                                                                                                                                                                                                          Combines two arrays into an array of pairs in which the first and second components are the corresponding elements of each input array. The resulting array is the length of the shorter of the input arrays.

                                                                                                                                                                                                                                                                                          Examples:

                                                                                                                                                                                                                                                                                          • #["Mon", "Tue", "Wed"].zip #[1, 2, 3] = #[("Mon", 1), ("Tue", 2), ("Wed", 3)]
                                                                                                                                                                                                                                                                                          • #["Mon", "Tue", "Wed"].zip #[1, 2] = #[("Mon", 1), ("Tue", 2)]
                                                                                                                                                                                                                                                                                          • #[x₁, x₂, x₃].zip #[y₁, y₂, y₃, y₄] = #[(x₁, y₁), (x₂, y₂), (x₃, y₃)]
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                            def Array.zipWithAll {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option αOption βγ) (as : Array α) (bs : Array β) :

                                                                                                                                                                                                                                                                                            Applies a function to the corresponding elements of both arrays, stopping when there are no more elements in either array. If one array is shorter than the other, the function is passed none for the missing elements.

                                                                                                                                                                                                                                                                                            Examples:

                                                                                                                                                                                                                                                                                            • #[1, 6].zipWithAll min #[5, 2] = #[some 1, some 2]
                                                                                                                                                                                                                                                                                            • #[1, 2, 3].zipWithAll Prod.mk #[5, 6] = #[(some 1, some 5), (some 2, some 6), (some 3, none)]
                                                                                                                                                                                                                                                                                            • #[x₁, x₂].zipWithAll f #[y] = #[f (some x₁) (some y), f (some x₂) none]
                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              @[irreducible]
                                                                                                                                                                                                                                                                                              def Array.zipWithAll.go {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option αOption βγ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                def Array.unzip {α : Type u} {β : Type u_1} (as : Array (α × β)) :
                                                                                                                                                                                                                                                                                                Array α × Array β

                                                                                                                                                                                                                                                                                                Separates an array of pairs into two arrays that contain the respective first and second components.

                                                                                                                                                                                                                                                                                                Examples:

                                                                                                                                                                                                                                                                                                • #[("Monday", 1), ("Tuesday", 2)].unzip = (#["Monday", "Tuesday"], #[1, 2])
                                                                                                                                                                                                                                                                                                • #[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzip = (#[x₁, x₂, x₃], #[y₁, y₂, y₃])
                                                                                                                                                                                                                                                                                                • (#[] : Array (Nat × String)).unzip = ((#[], #[]) : List Nat × List String)
                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  @[deprecated Array.partition (since := "2024-11-06")]
                                                                                                                                                                                                                                                                                                  def Array.split {α : Type u} (as : Array α) (p : αBool) :
                                                                                                                                                                                                                                                                                                  Array α × Array α
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                    def Array.replace {α : Type u} [BEq α] (xs : Array α) (a b : α) :

                                                                                                                                                                                                                                                                                                    Replaces the first occurrence of a with b in an array. The modification is performed in-place when the reference to the array is unique. Returns the array unmodified when a is not present.

                                                                                                                                                                                                                                                                                                    Examples:

                                                                                                                                                                                                                                                                                                    • #[1, 2, 3, 2, 1].replace 2 5 = #[1, 5, 3, 2, 1]
                                                                                                                                                                                                                                                                                                    • #[1, 2, 3, 2, 1].replace 0 5 = #[1, 2, 3, 2, 1]
                                                                                                                                                                                                                                                                                                    • #[].replace 2 5 = #[]
                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                      Lexicographic ordering #

                                                                                                                                                                                                                                                                                                      instance Array.instLT {α : Type u} [LT α] :
                                                                                                                                                                                                                                                                                                      LT (Array α)
                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      instance Array.instLE {α : Type u} [LT α] :
                                                                                                                                                                                                                                                                                                      LE (Array α)
                                                                                                                                                                                                                                                                                                      Equations

                                                                                                                                                                                                                                                                                                      Auxiliary functions used in metaprogramming. #

                                                                                                                                                                                                                                                                                                      We do not currently intend to provide verification theorems for these functions.

                                                                                                                                                                                                                                                                                                      leftpad and rightpad #

                                                                                                                                                                                                                                                                                                      def Array.leftpad {α : Type u} (n : Nat) (a : α) (xs : Array α) :

                                                                                                                                                                                                                                                                                                      Pads xs : Array α on the left with repeated occurrences of a : α until it is of size n. If xs already has at least n elements, it is returned unmodified.

                                                                                                                                                                                                                                                                                                      Examples:

                                                                                                                                                                                                                                                                                                      • #[1, 2, 3].leftpad 5 0 = #[0, 0, 1, 2, 3]
                                                                                                                                                                                                                                                                                                      • #["red", "green", "blue"].leftpad 4 "blank" = #["blank", "red", "green", "blue"]
                                                                                                                                                                                                                                                                                                      • #["red", "green", "blue"].leftpad 3 "blank" = #["red", "green", "blue"]
                                                                                                                                                                                                                                                                                                      • #["red", "green", "blue"].leftpad 1 "blank" = #["red", "green", "blue"]
                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                        def Array.rightpad {α : Type u} (n : Nat) (a : α) (xs : Array α) :

                                                                                                                                                                                                                                                                                                        Pads xs : Array α on the right with repeated occurrences of a : α until it is of length n. If l already has at least n elements, it is returned unmodified.

                                                                                                                                                                                                                                                                                                        Examples:

                                                                                                                                                                                                                                                                                                        • #[1, 2, 3].rightpad 5 0 = #[1, 2, 3, 0, 0]
                                                                                                                                                                                                                                                                                                        • #["red", "green", "blue"].rightpad 4 "blank" = #["red", "green", "blue", "blank"]
                                                                                                                                                                                                                                                                                                        • #["red", "green", "blue"].rightpad 3 "blank" = #["red", "green", "blue"]
                                                                                                                                                                                                                                                                                                        • #["red", "green", "blue"].rightpad 1 "blank" = #["red", "green", "blue"]
                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                          def Array.reduceOption {α : Type u} (as : Array (Option α)) :

                                                                                                                                                                                                                                                                                                          Drop nones from a Array, and replace each remaining some a with a.

                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                            eraseReps #

                                                                                                                                                                                                                                                                                                            def Array.eraseReps {α : Type u_1} [BEq α] (as : Array α) :

                                                                                                                                                                                                                                                                                                            Erases repeated elements, keeping the first element of each run.

                                                                                                                                                                                                                                                                                                            O(|as|).

                                                                                                                                                                                                                                                                                                            Example:

                                                                                                                                                                                                                                                                                                            • #[1, 3, 2, 2, 2, 3, 3, 5].eraseReps = #[1, 3, 2, 3, 5]
                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                              allDiff #

                                                                                                                                                                                                                                                                                                              def Array.allDiff {α : Type u} [BEq α] (as : Array α) :

                                                                                                                                                                                                                                                                                                              Returns true if no two elements of as are equal according to the == operator.

                                                                                                                                                                                                                                                                                                              Examples:

                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                getEvenElems #

                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                def Array.getEvenElems {α : Type u} (as : Array α) :

                                                                                                                                                                                                                                                                                                                Returns a new array that contains the elements at even indices in as, starting with the element at index 0.

                                                                                                                                                                                                                                                                                                                Examples:

                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                  Repr and ToString #

                                                                                                                                                                                                                                                                                                                  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