| changeset 1376 | 92f83b9d17e1 |
| parent 1151 | c820b3cc3df0 |
| child 1476 | 608483c2122a |
| 1375:d04af07266e8 | 1376:92f83b9d17e1 |
|---|---|
6 Quicksort |
6 Quicksort |
7 *) |
7 *) |
8 |
8 |
9 Qsort = Sorting + |
9 Qsort = Sorting + |
10 consts |
10 consts |
11 qsort :: "[['a,'a] => bool, 'a list] => 'a list" |
11 qsort :: [['a,'a] => bool, 'a list] => 'a list |
12 |
12 |
13 rules |
13 rules |
14 |
14 |
15 qsort_Nil "qsort le [] = []" |
15 qsort_Nil "qsort le [] = []" |
16 qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ |
16 qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ |