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
    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
        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
            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
                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
                    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
                        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
                            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
                                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
                                    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
                                        Instances For
                                          @[inline]
                                          def Subarray.isEmpty {α : Type u_1} (as : Subarray α) :

                                          Check whether a subarray is empty.

                                          Equations
                                            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
                                                    Instances For