eedaa56 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1406 from jthemphill/fix-qsort

eedaa56David Christiansen12 years ago

test/totality003/totality003.idr+1−1

compare with master

@@ -3,5 +3,5 @@ module smaller

3total

3total

4qsort : Ord a => List a -> List a

4qsort : Ord a => List a -> List a

5qsort [] = []

5qsort [] = []

6−qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++

6+qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++

7 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))

7 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))

test/totality003/totality003a.idr+1−1

@@ -3,5 +3,5 @@ module smaller

3total

3total

4qsort : Ord a => List a -> List a

4qsort : Ord a => List a -> List a

5qsort [] = []

5qsort [] = []

6−qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++

6+qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++

7 (x :: qsort (filter (>= x) xs))

7 (x :: qsort (filter (>= x) xs))