[isabelle] learning isabelle



Just trying to learn isabelle and had trouble with the following:

primrec
"checksort (x#y#zs) = ((x <= y) \<and> (checksort (y#zs)))"
"checksort _ = True"

The error is: "illegal argument in pattern". If someone could explain why this causes an error or how to repair it I'd appreciate that very much.

Cheers,
Ruben






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