Documentation

Batteries.Data.Array.Merge

def Array.merge {α : Type u_1} (lt : ααBool) (xs : Array α) (ys : Array α) :

O(|xs| + |ys|). Merge arrays xs and ys. If the arrays are sorted according to lt, then the result is sorted as well. If two (or more) elements are equal according to lt, they are preserved.

Equations
Instances For
    @[irreducible]
    def Array.merge.go {α : Type u_1} (lt : ααBool) (xs : Array α) (ys : Array α) (acc : Array α) (i : Nat) (j : Nat) :

    Auxiliary definition for merge.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[deprecated Array.merge]
      def Array.mergeSortedPreservingDuplicates {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) :

      O(|xs| + |ys|). Merge arrays xs and ys. If the arrays are sorted according to lt, then the result is sorted as well. If two (or more) elements are equal according to lt, they are preserved.

      Equations
      • xs.mergeSortedPreservingDuplicates ys = Array.merge (fun (x x_1 : α) => (compare x x_1).isLT) xs ys
      Instances For
        def Array.mergeDedupWith {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) (merge : ααα) :

        O(|xs| + |ys|). Merge arrays xs and ys, which must be sorted according to compare and must not contain duplicates. Equal elements are merged using merge. If merge respects the order (i.e. for all x, y, y', z, if x < y < z and x < y' < z then x < merge y y' < z) then the resulting array is again sorted.

        Equations
        Instances For
          @[irreducible]
          def Array.mergeDedupWith.go {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) (merge : ααα) (acc : Array α) (i : Nat) (j : Nat) :

          Auxiliary definition for mergeDedupWith.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[deprecated Array.mergeDedupWith]
            def Array.mergeSortedMergingDuplicates {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) (merge : ααα) :

            Alias of Array.mergeDedupWith.


            O(|xs| + |ys|). Merge arrays xs and ys, which must be sorted according to compare and must not contain duplicates. Equal elements are merged using merge. If merge respects the order (i.e. for all x, y, y', z, if x < y < z and x < y' < z then x < merge y y' < z) then the resulting array is again sorted.

            Equations
            Instances For
              @[inline]
              def Array.mergeDedup {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) :

              O(|xs| + |ys|). Merge arrays xs and ys, which must be sorted according to compare and must not contain duplicates. If an element appears in both xs and ys, only one copy is kept.

              Equations
              • xs.mergeDedup ys = xs.mergeDedupWith ys fun (x x_1 : α) => x
              Instances For
                @[deprecated Array.mergeDedup]
                def Array.mergeSortedDeduplicating {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) :

                Alias of Array.mergeDedup.


                O(|xs| + |ys|). Merge arrays xs and ys, which must be sorted according to compare and must not contain duplicates. If an element appears in both xs and ys, only one copy is kept.

                Equations
                Instances For
                  def Array.mergeUnsortedDedup {α : Type u_1} [eq : BEq α] (xs : Array α) (ys : Array α) :

                  O(|xs| * |ys|). Merge xs and ys, which do not need to be sorted. Elements which occur in both xs and ys are only added once. If xs and ys do not contain duplicates, then neither does the result.

                  Equations
                  Instances For
                    @[inline]
                    def Array.mergeUnsortedDedup.go {α : Type u_1} [eq : BEq α] (xs : Array α) (ys : Array α) :

                    Auxiliary definition for mergeUnsortedDedup.

                    Equations
                    Instances For
                      @[deprecated Array.mergeUnsortedDedup]
                      def Array.mergeUnsortedDeduplicating {α : Type u_1} [eq : BEq α] (xs : Array α) (ys : Array α) :

                      Alias of Array.mergeUnsortedDedup.


                      O(|xs| * |ys|). Merge xs and ys, which do not need to be sorted. Elements which occur in both xs and ys are only added once. If xs and ys do not contain duplicates, then neither does the result.

                      Equations
                      Instances For
                        def Array.mergeAdjacentDups {α : Type u_1} [eq : BEq α] (f : ααα) (xs : Array α) :

                        O(|xs|). Replace each run [x₁, ⋯, xₙ] of equal elements in xs with f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ.

                        Equations
                        Instances For
                          @[irreducible]
                          def Array.mergeAdjacentDups.go {α : Type u_1} [eq : BEq α] (f : ααα) (xs : Array α) (acc : Array α) (i : Nat) (hd : α) :

                          Auxiliary definition for mergeAdjacentDups.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[deprecated Array.mergeAdjacentDups]
                            def Array.mergeAdjacentDuplicates {α : Type u_1} [eq : BEq α] (f : ααα) (xs : Array α) :

                            Alias of Array.mergeAdjacentDups.


                            O(|xs|). Replace each run [x₁, ⋯, xₙ] of equal elements in xs with f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ.

                            Equations
                            Instances For
                              def Array.dedupSorted {α : Type u_1} [eq : BEq α] (xs : Array α) :

                              O(|xs|). Deduplicate a sorted array. The array must be sorted with to an order which agrees with ==, i.e. whenever x == y then compare x y == .eq.

                              Equations
                              Instances For
                                @[deprecated Array.dedupSorted]
                                def Array.deduplicateSorted {α : Type u_1} [eq : BEq α] (xs : Array α) :

                                Alias of Array.dedupSorted.


                                O(|xs|). Deduplicate a sorted array. The array must be sorted with to an order which agrees with ==, i.e. whenever x == y then compare x y == .eq.

                                Equations
                                Instances For
                                  def Array.sortDedup {α : Type u_1} [ord : Ord α] (xs : Array α) :

                                  O(|xs| log |xs|). Sort and deduplicate an array.

                                  Equations
                                  • xs.sortDedup = let_fun this := ord.toBEq; (xs.qsort (fun (x x_1 : α) => (compare x x_1).isLT) 0).dedupSorted
                                  Instances For
                                    @[deprecated Array.sortDedup]
                                    def Array.sortAndDeduplicate {α : Type u_1} [ord : Ord α] (xs : Array α) :

                                    Alias of Array.sortDedup.


                                    O(|xs| log |xs|). Sort and deduplicate an array.

                                    Equations
                                    Instances For