A small (and out-of-date) battery of examples has been developed in the TFL/HOL instantiation.
fun qsort(R:order,[]) = [] | qsort(R, x::rst) = qsort,(R, filter(not o R x) rst) ++ [x] ++ qsort(R, filter(R x) rst)as is the following more efficient version, which uses a single pass to partition the input to recursive calls:
(* Partition a list into two sublists *) fun part(P,[], l1,l2) = (l1,l2) | part(P, h::rst, l1,l2) = if P h then part(P,rst, h::l1, l2) else part(P,rst, l1, h::l2); (* A faster quicksort *) fun fqsort(R:order,[]) = [] | fqsort(R, x::rst) = let (l1,l2) = part((\y. R y x), rst,[],[]) in fqsort(R,l1) ++ [x] ++ fqsort(R,l2)Syntax note: "\" is lambda abstraction; "++" is list concatenation; and "::" is the "cons" operation for lists.
fun gcd (0,y) = y | gcd (Suc x, 0) = Suc x | gcd (Suc x, Suc y) = if (y <= x) then gcd(x - y, Suc y) else gcd(Suc x, y - x);we get the following induction principle for reasoning about gcd:
|- !P. (!y. P(0,y)) /\ (!x. P(Suc x,0)) /\ (!x y. (~(y <= x) ==> P(Suc x, y - x)) /\ (y <= x ==> P(x - y, Suc y)) ==> P (Suc x,Suc y)) ==> !v v1. P(v,v1)Syntax note: "!" is universal quantification; "/\" is conjunction; "~" is negation, and "==>" is implication.