Documentation

Batteries.Data.Array.Basic

Definitions on Arrays #

This file contains various definitions on Array. It does not contain proofs about these definitions, those are contained in other files in Batteries.Data.Array.

def Array.equalSet {α : Type u_1} [BEq α] (xs ys : Array α) :

Check whether xs and ys are equal as sets, i.e. they contain the same elements when disregarding order and duplicates. O(n*m)! If your element type has an Ord instance, it is asymptotically more efficient to sort the two arrays, remove duplicates and then compare them elementwise.

Equations
  • xs.equalSet ys = ((xs.all fun (x : α) => ys.contains x) && ys.all fun (x : α) => xs.contains x)
Instances For
    @[inline]
    def Array.minWith {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : Nat := xs.size) :
    α

    Returns the first minimal element among d and elements of the array. If start and stop are given, only the subarray xs[start:stop] is considered (in addition to d).

    Equations
    • xs.minWith d start stop = Array.foldl (fun (min x : α) => if (compare x min).isLT = true then x else min) d xs start stop
    Instances For
      @[inline]
      def Array.minD {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : Nat := xs.size) :
      α

      Find the first minimal element of an array. If the array is empty, d is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

      Equations
      • xs.minD d start stop = if h : start < xs.size start < stop then xs.minWith (xs.get start, ) (start + 1) stop else d
      Instances For
        @[inline]
        def Array.min? {α : Type u_1} [ord : Ord α] (xs : Array α) (start : Nat := 0) (stop : Nat := xs.size) :

        Find the first minimal element of an array. If the array is empty, none is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

        Equations
        • xs.min? start stop = if h : start < xs.size start < stop then some (xs.minD (xs.get start, ) start stop) else none
        Instances For
          @[inline]
          def Array.minI {α : Type u_1} [ord : Ord α] [Inhabited α] (xs : Array α) (start : Nat := 0) (stop : Nat := xs.size) :
          α

          Find the first minimal element of an array. If the array is empty, default is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

          Equations
          • xs.minI start stop = xs.minD default start stop
          Instances For
            @[inline]
            def Array.maxWith {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : Nat := xs.size) :
            α

            Returns the first maximal element among d and elements of the array. If start and stop are given, only the subarray xs[start:stop] is considered (in addition to d).

            Equations
            • xs.maxWith d start stop = xs.minWith d start stop
            Instances For
              @[inline]
              def Array.maxD {α : Type u_1} [ord : Ord α] (xs : Array α) (d : α) (start : Nat := 0) (stop : Nat := xs.size) :
              α

              Find the first maximal element of an array. If the array is empty, d is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

              Equations
              • xs.maxD d start stop = xs.minD d start stop
              Instances For
                @[inline]
                def Array.max? {α : Type u_1} [ord : Ord α] (xs : Array α) (start : Nat := 0) (stop : Nat := xs.size) :

                Find the first maximal element of an array. If the array is empty, none is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

                Equations
                • xs.max? start stop = xs.min? start stop
                Instances For
                  @[inline]
                  def Array.maxI {α : Type u_1} [ord : Ord α] [Inhabited α] (xs : Array α) (start : Nat := 0) (stop : Nat := xs.size) :
                  α

                  Find the first maximal element of an array. If the array is empty, default is returned. If start and stop are given, only the subarray xs[start:stop] is considered.

                  Equations
                  • xs.maxI start stop = xs.minI start stop
                  Instances For
                    @[deprecated Array.flatten]
                    def Array.join {α : Type u} (as : Array (Array α)) :

                    Alias of Array.flatten.


                    Joins array of array into a single array.

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

                    Equations
                    Instances For

                      Safe Nat Indexed Array functions #

                      The functions in this section offer variants of Array functions which use Nat indices instead of Fin indices. All these functions have as parameter a proof that the index is valid for the array. But this parameter has a default argument by get_elem_tactic which should prove the index bound.

                      @[reducible, inline]
                      abbrev Array.setN {α : Type u_1} (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :

                      setN a i h x sets an element in a vector using a Nat index which is provably valid. A proof by get_elem_tactic is provided as a default argument for h. This will perform the update destructively provided that a has a reference count of 1 when called.

                      Equations
                      • a.setN i x h = a.set i, h x
                      Instances For
                        @[reducible, inline]
                        abbrev Array.swapN {α : Type u_1} (a : Array α) (i j : Nat) (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) :

                        swapN a i j hi hj swaps two Nat indexed entries in an Array α. Uses get_elem_tactic to supply a proof that the indices are in range. hi and hj are both given a default argument by get_elem_tactic. This will perform the update destructively provided that a has a reference count of 1 when called.

                        Equations
                        • a.swapN i j hi hj = a.swap i, hi j, hj
                        Instances For
                          @[reducible, inline]
                          abbrev Array.swapAtN {α : Type u_1} (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
                          α × Array α

                          swapAtN a i h x swaps the entry with index i : Nat in the vector for a new entry x. The old entry is returned alongwith the modified vector. Automatically generates proof of i < a.size with get_elem_tactic where feasible.

                          Equations
                          • a.swapAtN i x h = a.swapAt i, h x
                          Instances For
                            @[reducible, inline]
                            abbrev Array.eraseIdxN {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) :

                            eraseIdxN a i h Removes the element at position i from a vector of length n. h : i < a.size has a default argument by get_elem_tactic which tries to supply a proof that the index is valid. This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

                            Equations
                            • a.eraseIdxN i h = a.feraseIdx i, h
                            Instances For
                              def Array.eraseIdx! {α : Type u_1} (a : Array α) (i : Nat) :

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Array.finRange (n : Nat) :

                                finRange n is the array of all elements of Fin n in order.

                                Equations
                                Instances For
                                  @[inline]
                                  def Subarray.isEmpty {α : Type u_1} (as : Subarray α) :

                                  Check whether a subarray is empty.

                                  Equations
                                  • as.isEmpty = (as.start == as.stop)
                                  Instances For
                                    @[inline]
                                    def Subarray.contains {α : Type u_1} [BEq α] (as : Subarray α) (a : α) :

                                    Check whether a subarray contains an element.

                                    Equations
                                    Instances For
                                      def Subarray.popHead? {α : Type u_1} (as : Subarray α) :

                                      Remove the first element of a subarray. Returns the element and the remaining subarray, or none if the subarray is empty.

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