Definition of merge
and mergeSort
. #
These definitions are intended for verification purposes,
and are replaced at runtime by efficient versions in Init.Data.List.Sort.Impl
.
Merges two lists, using le
to select the first element of the resulting list if both are
non-empty.
If both input lists are sorted according to le
, then the resulting list is also sorted according
to le
. O(|xs| + |ys|)
.
This implementation is not tail-recursive, but it is replaced at runtime by a proven-equivalent tail-recursive merge.
A stable merge sort.
This function is a simplified implementation that's designed to be easy to reason about, rather than
for efficiency. In particular, it uses the non-tail-recursive List.merge
function and traverses
lists unnecessarily.
It is replaced at runtime by an efficient implementation that has been proven to be equivalent.
Given an ordering relation le : α → α → Bool
,
construct the lexicographic ordering on α × Nat
.
which first compares the first components using le
,
but if these are equivalent (in the sense le a.2 b.2 && le b.2 a.2
)
then compares the second components using ≤
.
This function is only used in stating the stability properties of mergeSort
.