ink

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

Merge arrays xs and ys, which must be sorted according to compare. The result is sorted as well. If two (or more) elements are equal according to compare, they are preserved.

Equations

• Array.mergeSortedPreservingDuplicates xs ys = let acc := Array.mkEmpty (Array.size xs + Array.size ys); Array.mergeSortedPreservingDuplicates.go xs ys acc 0 0

ink

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

Auxiliary definition for mergeSortedPreservingDuplicates.

Equations

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

ink

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

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 xs ys merge = let acc := Array.mkEmpty (Array.size xs + Array.size ys); Array.mergeSortedMergingDuplicates.go xs ys merge acc 0 0

ink

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

Auxiliary definition for mergeSortedMergingDuplicates.

Equations

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

ink

@[inline]

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

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 xs ys = Array.mergeSortedMergingDuplicates xs ys fun x x_1 => x

ink

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

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. O(n*m)!

Equations

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

ink

@[inline]

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

Auxiliary definition for mergeUnsortedDeduplicating.

Equations

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

ink

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

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

Equations

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

ink

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

Auxiliary definition for mergeAdjacentDuplicates.

Equations

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

ink

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

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 xs = Array.mergeAdjacentDuplicates (fun x x_1 => x) xs

ink

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

Sort and deduplicate an array.

Equations

• Array.sortAndDeduplicate xs = let_fun this := Ord.toBEq ord; Array.deduplicateSorted (Array.qsort xs (fun x x_1 => Ordering.isLT (compare x x_1)) 0 (Array.size xs - 1))