idris-lang/idris-tutorial — pull request #36 by jthemphill (2014-07-17 08:19:31+00:00)
Title: Fix qsort implementation in totality section

The current implementation of qsort here double counts instances of x... we should fix that.

On a different note... I feel like in the future we shouldn't need `assert_smaller` here at all, since `xs` is guaranteed to be smaller than `x :: xs` (and filter can never make a list larger).