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.

## Instances For

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.

## Instances For

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)!

## Instances For

@[inline]

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

Array α

Auxiliary definition for `mergeUnsortedDeduplicating`

.

## Instances For

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.