module Main
%default total
%hide merge
%hide sort
merge : Ord a => List a -> List a -> List a
merge Nil b = b
merge a Nil = a
merge (a :: as) (b :: bs) =
if a < b then a :: merge as (b :: bs)
else b :: merge (a :: as) bs
sort : Ord a => List a -> List a
sort Nil = Nil
sort [x] = [x]
sort xs = assert_total $
let n = length xs `div` 2 in
sort (take n xs) `merge` sort (drop n xs)
main : IO ()
main = do
printLn $ sort (the (List Nat) [])
printLn $ sort [1]
printLn $ sort [1, 2, 3, 4]
printLn $ sort [5, 2, 8, 6]
printLn $ sort [8, 2, 5, 6, 6, 5, 4]
