Re: [isabelle] div instances?



John Matthews wrote:
but when I give Isar this command,

  instance lift :: (div)div ..

Isabelle responds with this syntax error message:

  *** Inner syntax error at: "div"
  *** Expected tokens:  "{" "{}" "longid" "id"
  *** At command "instance".

It seems that the Isabelle parser confuses the infix "div" operator
with the "div" type class. To circumvent this problem, you can prefix
"div" with the name of the theory "Divides" in which it is declared, i.e.

instance lift :: (Divides.div)Divides.div ..

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.