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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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