def Array.merge {α : Type u_1} (lt : α → α → Bool) (xs : Array α) (ys : Array α) : 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

• Array.merge lt xs ys = Array.merge.go lt xs ys (Array.mkEmpty (Array.size xs + Array.size ys)) 0 0

def Array.merge.go {α : Type u_1} (lt : α → α → Bool) (xs : Array α) (ys : Array α) (acc : Array α) (i : Nat) (j : Nat) : Array α

Auxiliary definition for merge.

Equations

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

@[deprecated Array.merge]

def Array.mergeSortedPreservingDuplicates {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) : 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

• Array.mergeSortedPreservingDuplicates xs ys = Array.merge (fun (x x_1 : α) => Ordering.isLT (compare x x_1)) xs ys

def Array.mergeDedupWith {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) (merge : α → α → α) : Array α

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

• Array.mergeDedupWith xs ys merge = Array.mergeDedupWith.go xs ys merge (Array.mkEmpty (Array.size xs + Array.size ys)) 0 0

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

Auxiliary definition for mergeDedupWith.

Equations

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

@[deprecated Array.mergeDedupWith]

def Array.mergeSortedMergingDuplicates {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) (merge : α → α → α) : Array α

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

• @Array.mergeSortedMergingDuplicates = @Array.mergeDedupWith

@[inline]

def Array.mergeDedup {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) : 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

• Array.mergeDedup xs ys = Array.mergeDedupWith xs ys fun (x x_1 : α) => x

@[deprecated Array.mergeDedup]

def Array.mergeSortedDeduplicating {α : Type u_1} [ord : Ord α] (xs : Array α) (ys : Array α) : 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

• @Array.mergeSortedDeduplicating = @Array.mergeDedup

def Array.mergeUnsortedDedup {α : Type u_1} [eq : BEq α] (xs : Array α) (ys : Array α) : 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

• Array.mergeUnsortedDedup xs ys = if Array.size xs < Array.size ys then Array.mergeUnsortedDedup.go ys xs else Array.mergeUnsortedDedup.go xs ys

@[inline]

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

Auxiliary definition for mergeUnsortedDedup.

Equations

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

@[deprecated Array.mergeUnsortedDedup]

def Array.mergeUnsortedDeduplicating {α : Type u_1} [eq : BEq α] (xs : Array α) (ys : Array α) : 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

• @Array.mergeUnsortedDeduplicating = @Array.mergeUnsortedDedup

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

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

Equations

• Array.mergeAdjacentDups f xs = if h : 0 < Array.size xs then Array.mergeAdjacentDups.go f xs (Array.mkEmpty (Array.size xs)) 1 (Array.get xs { val := 0, isLt := h }) else xs

def Array.mergeAdjacentDups.go {α : Type u_1} [eq : BEq α] (f : α → α → α) (xs : Array α) (acc : Array α) (i : Nat) (hd : α) : Array α

Auxiliary definition for mergeAdjacentDups.

Equations

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

@[deprecated Array.mergeAdjacentDups]

def Array.mergeAdjacentDuplicates {α : Type u_1} [eq : BEq α] (f : α → α → α) (xs : Array α) : 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

• @Array.mergeAdjacentDuplicates = @Array.mergeAdjacentDups

def Array.dedupSorted {α : Type u_1} [eq : BEq α] (xs : Array α) : 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

• Array.dedupSorted xs = Array.mergeAdjacentDups (fun (x x_1 : α) => x) xs

@[deprecated Array.dedupSorted]

def Array.deduplicateSorted {α : Type u_1} [eq : BEq α] (xs : Array α) : 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

• @Array.deduplicateSorted = @Array.dedupSorted

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

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

Equations

• Array.sortDedup xs = let_fun this := Ord.toBEq ord; Array.dedupSorted (Array.qsort xs (fun (x x_1 : α) => Ordering.isLT (compare x x_1)) 0)

@[deprecated Array.sortDedup]

def Array.sortAndDeduplicate {α : Type u_1} [ord : Ord α] (xs : Array α) : Array α

Alias of Array.sortDedup.

---

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

Equations

• @Array.sortAndDeduplicate = @Array.sortDedup