idris-mergesort

Verified implementation of a total mergesort in Idris in under 133 loc. The type signature of the mergesort function is total mergeSort : (xs : List Nat) -> (ys : List Nat ** (Ordered ys, Permutation xs ys)), where the definition of the type families Ordered and Permutation are borrowed from the standard library of Coq. mergeSort is only defined on lists of natural numbers, because it seems Idris standard library lacks a type class for decidable orderability (similar to DecEq). The time complexity of the mergeSort function is probably higher than O(n*log(n)) since the split function used, which is from Idris standard library, has time complexity O(n*log(n)).