[isabelle-dev] Code export to Haskell and lower-case theory names

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Mar 29 19:00:53 CET 2013

Hi Manuel,

> 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.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130329/c56ab2ad/attachment.sig>

More information about the isabelle-dev mailing list