[isabelle-dev] Bug report: code generation for eq with indirect-recursive datatypes
florian.haftmann at informatik.tu-muenchen.de
Mon Feb 23 23:42:05 CET 2009
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev