[isabelle-dev] Code export to Haskell and lower-case theory names
huffman at in.tum.de
Fri Mar 29 23:32:58 CET 2013
On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner <breitner at kit.edu> wrote:
> 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:
> 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.
More information about the isabelle-dev