31 |
31 |
32 insert_def "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)" |
32 insert_def "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)" |
33 isort_def "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))" |
33 isort_def "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))" |
34 |
34 |
35 partition_def |
35 partition_def |
36 "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.\ |
36 "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs. |
37 \ if f`x then part(xs,x$a,b) else part(xs,a,x$b)) \ |
37 if f`x then part(xs,x$a,b) else part(xs,a,x$b)) |
38 \ in part(l,[],[])" |
38 in part(l,[],[])" |
39 qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. \ |
39 qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. |
40 \ let p be partition(f`h,t) \ |
40 let p be partition(f`h,t) |
41 \ in split(p,%x y.qsortx(x) @ h$qsortx(y))) \ |
41 in split(p,%x y.qsortx(x) @ h$qsortx(y))) |
42 \ in qsortx(l)" |
42 in qsortx(l)" |
43 |
43 |
44 end |
44 end |