Temporarily disable buffer001 test

Seems to have a problem on 32 bit machines? Or at least, segfaults
inexplicably on some machines.
Add assert_smaller function

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.
Merge branch 'master' of github.com:idris-lang/Idris-dev