So don't write quicksort in Idris. It's not going to work very well anyways. It's not at all well-suited, and isn't really even an especially important sorting

So don't write quicksort in Idris. It's not going to work very well anyways. It's not at all well-suited, and isn't really even an especially important sorting algorithm in a world where linear time sorting and constant time indexed searches are a thing. But most of the work you'd be doing to write quicksort is writing the machinery for structurally recursive sorting, which a lot of tutorials write not because you have to, but because it's a very good exercise for learning how to write total functions that are recursive in a way DT systems can prove totality on. Most of these tools are in the contrib library (and the book mentions this). For example the preorder interface you need: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Decidable/Order.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/con...