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.