[isabelle] Basic use of lists


Could someone please tell me what is wrong with:

consts sortL2 :: "int list ⇒ int list"
"sortL2 [] = []"
"sortL2 (x#xs) = (case xs of [] ⇒ [x] | y # ys ⇒ (if (x < y) then (y#(sortL2 (x#(ys)))) else (x#(sortL2 (y#ys))))) "

No matter how I turn it I either get a type unification error or a constant defined on RHS error.

Thanks for your time.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.