Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation Module Cycles


view this post on Zulip 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: Mar 28 2024 at 12:29 UTC