[etatoby]

Try to write the classic Haskell Quicksort in Idris:

    qsort :: Ord a => [a] -> [a]
    qsort [] = []
    qsort (p:xs) = qsort (filter (< p) xs) ++ [p] ++ qsort (filter (>= p) xs)

and let me know how it goes, if you will. That's when I gave up on Idris.

[AzzieElbab]

This one liner isn't really quicksort anyway.