Re: [isabelle] Code generation Module Cycles



Hi David,

which Isabelle version are you using?  The generation of a module
Integer.hs is strange since Isabelle2009-1 has no theory Integer.thy and
the theories Int.thy and Nat.thy are mapped to Arith.hs by default
(among other arithmetic theories, which solves the problem of cyclic
module dependencies for most cases).

When exporting code, you can ignore modules entirely by using an
explicit module name

export_code ... in Haskell module_name ... file ...

Hope this helps,
	Florian

-- 

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

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

Attachment: signature.asc
Description: OpenPGP digital signature



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