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

[Florian Haftmann]

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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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