Data.SBV.Plugin.Examples.MergeSort

Implementing merge-sort

merge

mergeSort

Proving correctness of sorting

nonDecreasing

isPermutationOf

The correctness theorem

mergeSortCorrect