assert_smaller x y evaluates to y, and asserts to the totality checker
than y is structurally smaller than x. This can be used to explain the
reasoning for totality if the checker cannot work it out itself. For
example:
total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
The expression 'assert_smaller (x :: xs) (filter (<= x) xs)' asserts
that the result of the filter will always be smaller than the pattern
(x :: xs).
Using this is always preferable to %assert_total if the termination
argument can be explained in this way.
