Re: [isabelle] learning isabelle



Ruben Henner Zilibowitz wrote:
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.

Patterns containing "_" are currently not supported by primrec. You
can repair your definition by replacing "_" by a variable, e.g. x.

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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