[isabelle-dev] Bug report: code generation for eq with indirect-recursive datatypes

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Feb 23 23:42:05 CET 2009

Hi Brian,

> However, if I try to generate OCaml or SML code, the second one still
> fails, but with a different error this time:
> *** Illegal mutual dependencies: "tree :: eq", "eq_class.eq [tree]"
> *** At command "export_code".
> What do you think?

This is the situation as reported in sect. 1.2.6 of the code generation
tutorial (repository version), and exactly the reason why the explicit
theorem for eq using list_all is provided.  Some day I plan to replace
those naive theorems eq by an explicit interpretation of the
construction of the datatype which does not induce mutual dependencies
between inst and fun statements anyway.

Hope this helps



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090223/81e22fb5/attachment.sig>

More information about the isabelle-dev mailing list