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

[Florian Haftmann]

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
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>