[isabelle-dev] Code export to Haskell and lower-case theory names
florian.haftmann at informatik.tu-muenchen.de
Fri Mar 29 19:00:53 CET 2013
> I just noticed that when exporting code to Haskell, there is a
> complication when some of the theories involved have lower-case names.
> The code export itself will work with no error or warning, but when
> ghc/ghci are invoked on the generated code, they will report the
> lower-case module name of the module that corresponds to the theory as a
> parse error, as Haskell apparently does not allow lower-case module names.
maybe it never worked that way, maybe it never got noticed. However,
the produced module names should indeed be valid wrt. to the underlying
target language. I have some reform related to code naming on my
agenda, where I can reexamine and amend this.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev