Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation Module Cycles

Email Gateway (Aug 18 2022 at 14:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC