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

Manuel Eberl eberlm at in.tum.de
Thu Mar 28 19:19:58 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.

Is this a known issue, or even intended behaviour? I think the code
export tool should automatically rename this to an upper case version,
similarly to what it does with name clashes and Unicode tokens in
identifiers, or at least abort with an error message.


More information about the isabelle-dev mailing list