Documentation

Init.Data.Array.Basic

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

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

        Equations
        Instances For
          Equations
          • Array.instGetElemArrayUSizeLtNatInstLTNatToNatSize = { getElem := fun xs i h => Array.uget xs i h }
          def Array.back {α : Type u} [Inhabited α] (a : Array α) :
          α
          Equations
          Instances For
            def Array.get? {α : Type u} (a : Array α) (i : Nat) :
            Equations
            Instances For
              def Array.back? {α : Type u} (a : Array α) :
              Equations
              Instances For
                @[inline, reducible]
                abbrev Array.getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : Array.size a = n) (h₂ : i < n) :
                α
                Equations
                Instances For
                  @[simp]
                  theorem Array.size_set {α : Type u} (a : Array α) (i : Fin (Array.size a)) (v : α) :
                  @[simp]
                  theorem Array.size_push {α : Type u} (a : Array α) (v : α) :
                  @[extern lean_array_uset]
                  def Array.uset {α : Type u} (a : Array α) (i : USize) (v : α) (h : USize.toNat i < Array.size a) :

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

                  Equations
                  Instances For
                    @[extern lean_array_fswap]
                    def Array.swap {α : Type u} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) :
                    Equations
                    Instances For
                      @[extern lean_array_swap]
                      def Array.swap! {α : Type u} (a : Array α) (i : Nat) (j : Nat) :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[inline]
                        def Array.swapAt {α : Type u} (a : Array α) (i : Fin (Array.size a)) (v : α) :
                        α × Array α
                        Equations
                        Instances For
                          @[inline]
                          def Array.swapAt! {α : Type u} (a : Array α) (i : Nat) (v : α) :
                          α × Array α
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[extern lean_array_pop]
                            def Array.pop {α : Type u} (a : Array α) :
                            Equations
                            Instances For
                              def Array.shrink {α : Type u} (a : Array α) (n : Nat) :
                              Equations
                              Instances For
                                def Array.shrink.loop {α : Type u} :
                                NatArray αArray α
                                Equations
                                Instances For
                                  @[inline]
                                  unsafe def Array.modifyMUnsafe {α : Type u} {m : Type u → Type u_1} [Monad m] (a : Array α) (i : Nat) (f : αm α) :
                                  m (Array α)
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[implemented_by Array.modifyMUnsafe]
                                    def Array.modifyM {α : Type u} {m : Type u → Type u_1} [Monad m] (a : Array α) (i : Nat) (f : αm α) :
                                    m (Array α)
                                    Equations
                                    Instances For
                                      @[inline]
                                      def Array.modify {α : Type u} (a : Array α) (i : Nat) (f : αα) :
                                      Equations
                                      Instances For
                                        @[inline]
                                        def Array.modifyOp {α : Type u} (self : Array α) (idx : Nat) (f : αα) :
                                        Equations
                                        Instances For
                                          @[inline]
                                          unsafe def Array.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : αβm (ForInStep β)) :
                                          m β

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

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

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

                                              Reference implementation for forIn

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

                                                  See comment at forInUnsafe

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

                                                      Reference implementation for foldlM

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

                                                          See comment at forInUnsafe

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

                                                              Reference implementation for foldrM

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

                                                                  See comment at forInUnsafe

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

                                                                      Reference implementation for mapM

                                                                      Equations
                                                                      Instances For
                                                                        def Array.mapM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αm β) (as : Array α) (i : Nat) (r : Array β) :
                                                                        m (Array β)
                                                                        Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def Array.mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin (Array.size as)αm β) :
                                                                          m (Array β)
                                                                          Equations
                                                                          Instances For
                                                                            @[specialize #[]]
                                                                            def Array.mapIdxM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin (Array.size as)αm β) (i : Nat) (j : Nat) (inv : i + j = Array.size as) (bs : Array β) :
                                                                            m (Array β)
                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Array.findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αm (Option β)) :
                                                                              m (Option β)
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[inline]
                                                                                def Array.findM? {α : Type} {m : TypeType} [Monad m] (as : Array α) (p : αm Bool) :
                                                                                m (Option α)
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Array.findIdxM? {α : Type u} {m : TypeType u_1} [Monad m] (as : Array α) (p : αm Bool) :
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    unsafe def Array.anyMUnsafe {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[specialize #[]]
                                                                                      unsafe def Array.anyMUnsafe.any {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (i : USize) (stop : USize) :
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[implemented_by Array.anyMUnsafe]
                                                                                        def Array.anyM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                        Equations
                                                                                        Instances For
                                                                                          def Array.anyM.loop {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (stop : Nat) (h : stop Array.size as) (j : Nat) :
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            @[inline]
                                                                                            def Array.allM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def Array.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αm (Option β)) :
                                                                                              m (Option β)
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[specialize #[]]
                                                                                                def Array.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : αm (Option β)) (i : Nat) :
                                                                                                i Array.size asm (Option β)
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Array.findRevM? {α : Type} {m : TypeType w} [Monad m] (as : Array α) (p : αm Bool) :
                                                                                                  m (Option α)
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    def Array.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      def Array.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Array α) (start : optParam Nat (Array.size as)) (stop : optParam Nat 0) :
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        def Array.foldl {α : Type u} {β : Type v} (f : βαβ) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                        β
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          def Array.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) (as : Array α) (start : optParam Nat (Array.size as)) (stop : optParam Nat 0) :
                                                                                                          β
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            def Array.map {α : Type u} {β : Type v} (f : αβ) (as : Array α) :
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              def Array.mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin (Array.size as)αβ) :
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                def Array.find? {α : Type} (as : Array α) (p : αBool) :
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  def Array.findSome? {α : Type u} {β : Type v} (as : Array α) (f : αOption β) :
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def Array.findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : αOption β) :
                                                                                                                    β
                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def Array.findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : αOption β) :
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]
                                                                                                                        def Array.findRev? {α : Type} (as : Array α) (p : αBool) :
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          def Array.findIdx? {α : Type u} (as : Array α) (p : αBool) :
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def Array.findIdx?.loop {α : Type u} (as : Array α) (p : αBool) (i : Nat) (j : Nat) (inv : i + j = Array.size as) :
                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              def Array.getIdx? {α : Type u} [BEq α] (a : Array α) (v : α) :
                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[inline]
                                                                                                                                def Array.any {α : Type u} (as : Array α) (p : αBool) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  @[inline]
                                                                                                                                  def Array.all {α : Type u} (as : Array α) (p : αBool) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    def Array.contains {α : Type u} [BEq α] (as : Array α) (a : α) :
                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      def Array.elem {α : Type u} [BEq α] (a : α) (as : Array α) :
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[inline]
                                                                                                                                        def Array.getEvenElems {α : Type u} (as : Array α) :
                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For
                                                                                                                                          @[export lean_array_to_list]
                                                                                                                                          def Array.toList {α : Type u} (as : Array α) :
                                                                                                                                          List α
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            instance Array.instReprArray {α : Type u} [Repr α] :
                                                                                                                                            Repr (Array α)
                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            instance Array.instToStringArray {α : Type u} [ToString α] :
                                                                                                                                            Equations
                                                                                                                                            def Array.append {α : Type u} (as : Array α) (bs : Array α) :
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              instance Array.instAppendArray {α : Type u} :
                                                                                                                                              Equations
                                                                                                                                              • Array.instAppendArray = { append := Array.append }
                                                                                                                                              def Array.appendList {α : Type u} (as : Array α) (bs : List α) :
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                instance Array.instHAppendArrayList {α : Type u} :
                                                                                                                                                HAppend (Array α) (List α) (Array α)
                                                                                                                                                Equations
                                                                                                                                                • Array.instHAppendArrayList = { hAppend := Array.appendList }
                                                                                                                                                @[inline]
                                                                                                                                                def Array.concatMapM {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : αm (Array β)) (as : Array α) :
                                                                                                                                                m (Array β)
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[inline]
                                                                                                                                                  def Array.concatMap {α : Type u} {β : Type u_1} (f : αArray β) (as : Array α) :
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For
                                                                                                                                                      @[specialize #[]]
                                                                                                                                                      def Array.isEqvAux {α : Type u_1} (a : Array α) (b : Array α) (hsz : Array.size a = Array.size b) (p : ααBool) (i : Nat) :
                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        def Array.isEqv {α : Type u_1} (a : Array α) (b : Array α) (p : ααBool) :
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          instance Array.instBEqArray {α : Type u_1} [BEq α] :
                                                                                                                                                          BEq (Array α)
                                                                                                                                                          Equations
                                                                                                                                                          • Array.instBEqArray = { beq := fun a b => Array.isEqv a b BEq.beq }
                                                                                                                                                          @[inline]
                                                                                                                                                          def Array.filter {α : Type u_1} (p : αBool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            def Array.filterM {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                                                                            m (Array α)
                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[specialize #[]]
                                                                                                                                                              def Array.filterMapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm (Option β)) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                                                                              m (Array β)
                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                def Array.filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[specialize #[]]
                                                                                                                                                                  def Array.getMax? {α : Type u_1} (as : Array α) (lt : ααBool) :
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    def Array.partition {α : Type u_1} (p : αBool) (as : Array α) :
                                                                                                                                                                    Array α × Array α
                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For
                                                                                                                                                                      theorem Array.ext {α : Type u_1} (a : Array α) (b : Array α) (h₁ : Array.size a = Array.size b) (h₂ : ∀ (i : Nat) (hi₁ : i < Array.size a) (hi₂ : i < Array.size b), a[i] = b[i]) :
                                                                                                                                                                      a = b
                                                                                                                                                                      theorem Array.ext.extAux {α : Type u_1} (a : List α) (b : List α) (h₁ : List.length a = List.length b) (h₂ : ∀ (i : Nat) (hi₁ : i < List.length a) (hi₂ : i < List.length b), List.get a { val := i, isLt := hi₁ } = List.get b { val := i, isLt := hi₂ }) :
                                                                                                                                                                      a = b
                                                                                                                                                                      theorem Array.extLit {α : Type u_1} {n : Nat} (a : Array α) (b : Array α) (hsz₁ : Array.size a = n) (hsz₂ : Array.size b = n) (h : ∀ (i : Nat) (hi : i < n), Array.getLit a i hsz₁ hi = Array.getLit b i hsz₂ hi) :
                                                                                                                                                                      a = b
                                                                                                                                                                      def Array.indexOfAux {α : Type u_1} [BEq α] (a : Array α) (v : α) (i : Nat) :
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        def Array.indexOf? {α : Type u_1} [BEq α] (a : Array α) (v : α) :
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem Array.size_swap {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) :
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem Array.size_pop {α : Type u_1} (a : Array α) :
                                                                                                                                                                          theorem Array.reverse.termination {i : Nat} {j : Nat} (h : i < j) :
                                                                                                                                                                          j - 1 - (i + 1) < j - i
                                                                                                                                                                          def Array.reverse {α : Type u_1} (as : Array α) :
                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            def Array.reverse.loop {α : Type u_1} (as : Array α) (i : Nat) (j : Fin (Array.size as)) :
                                                                                                                                                                            Equations
                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                            Instances For
                                                                                                                                                                              def Array.popWhile {α : Type u_1} (p : αBool) (as : Array α) :
                                                                                                                                                                              Equations
                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                              Instances For
                                                                                                                                                                                def Array.takeWhile {α : Type u_1} (p : αBool) (as : Array α) :
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  def Array.takeWhile.go {α : Type u_1} (p : αBool) (as : Array α) (i : Nat) (r : Array α) :
                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    def Array.eraseIdxAux {α : Type u_1} (i : Nat) (a : Array α) :
                                                                                                                                                                                    Equations
                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      def Array.feraseIdx {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) :
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        def Array.eraseIdx {α : Type u_1} (a : Array α) (i : Nat) :
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          def Array.eraseIdxSzAux {α : Type u_1} (a : Array α) (i : Nat) (r : Array α) (heq : Array.size r = Array.size a) :
                                                                                                                                                                                          { r // Array.size r = Array.size a - 1 }
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            def Array.eraseIdx' {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) :
                                                                                                                                                                                            { r // Array.size r = Array.size a - 1 }
                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              def Array.erase {α : Type u_1} [BEq α] (as : Array α) (a : α) :
                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                def Array.insertAt {α : Type u_1} (as : Array α) (i : Fin (Array.size as + 1)) (a : α) :

                                                                                                                                                                                                Insert element a at position i.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  def Array.insertAt.loop {α : Type u_1} (as : Array α) (i : Fin (Array.size as + 1)) (as : Array α) (j : Fin (Array.size as)) :
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    def Array.insertAt! {α : Type u_1} (as : Array α) (i : Nat) (a : α) :

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

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      def Array.toListLitAux {α : Type u_1} (a : Array α) (n : Nat) (hsz : Array.size a = n) (i : Nat) :
                                                                                                                                                                                                      i Array.size aList αList α
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        def Array.toArrayLit {α : Type u_1} (a : Array α) (n : Nat) (hsz : Array.size a = n) :
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          theorem Array.ext' {α : Type u_1} {as : Array α} {bs : Array α} (h : as.data = bs.data) :
                                                                                                                                                                                                          as = bs
                                                                                                                                                                                                          theorem Array.toArrayAux_eq {α : Type u_1} (as : List α) (acc : Array α) :
                                                                                                                                                                                                          (List.toArrayAux as acc).data = acc.data ++ as
                                                                                                                                                                                                          theorem Array.data_toArray {α : Type u_1} (as : List α) :
                                                                                                                                                                                                          (List.toArray as).data = as
                                                                                                                                                                                                          theorem Array.toArrayLit_eq {α : Type u_1} (as : Array α) (n : Nat) (hsz : Array.size as = n) :
                                                                                                                                                                                                          as = Array.toArrayLit as n hsz
                                                                                                                                                                                                          theorem Array.toArrayLit_eq.getLit_eq {α : Type u_1} (n : Nat) (as : Array α) (i : Nat) (h₁ : Array.size as = n) (h₂ : i < n) :
                                                                                                                                                                                                          Array.getLit as i h₁ h₂ = as.data[i]
                                                                                                                                                                                                          theorem Array.toArrayLit_eq.go {α : Type u_1} (as : Array α) (n : Nat) (hsz : Array.size as = n) (i : Nat) (hi : i Array.size as) :
                                                                                                                                                                                                          Array.toListLitAux as n hsz i hi (List.drop i as.data) = as.data
                                                                                                                                                                                                          def Array.isPrefixOfAux {α : Type u_1} [BEq α] (as : Array α) (bs : Array α) (hle : Array.size as Array.size bs) (i : Nat) :
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            def Array.isPrefixOf {α : Type u_1} [BEq α] (as : Array α) (bs : Array α) :

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

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def Array.allDiff {α : Type u_1} [BEq α] (as : Array α) :
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                @[specialize #[]]
                                                                                                                                                                                                                def Array.zipWithAux {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                  def Array.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : αβγ) :
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    def Array.zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :
                                                                                                                                                                                                                    Array (α × β)
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      def Array.unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) :
                                                                                                                                                                                                                      Array α × Array β
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        def Array.split {α : Type u_1} (as : Array α) (p : αBool) :
                                                                                                                                                                                                                        Array α × Array α
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For