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

[Brian Huffman]

On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner <breitner at kit.edu> wrote:
> Hi,
>
> Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius:
>> > This has got nothing to do with Isabelle's informal conventions but is
>> > all about the target language's formal rules.
>>
>> The conventions about theory names and locale/class names are not that
>> informal.  If you violate them systematically, certain name space policies
>> will break down.  That is then a "general user error".
>
> Are there really things that break if I deviate from the convention?

The main problem I know about is that qualified names can become
ambiguous: e.g. if "foo.bar.baz" and "bar.boo.baz" are both in scope,
then "bar.baz" could refer to either of them. The problem is avoided
if theory names and locale/type/constant names are kept disjoint. See
also this old thread:

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-July/001674.html

> Then it should be a hard rule enforced by the system. If that is not the
> case, then it should be fully supported and up to the user to choose his
> naming, even if it deviate from what others use (she might have reasons
> for that).

I completely agree.

- Brian