[isabelle-dev] Code export to Haskell and lower-case theory names
breitner at kit.edu
Fri Mar 29 23:44:33 CET 2013
Am Freitag, den 29.03.2013, 15:32 -0700 schrieb Brian Huffman:
> 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:
but in every case there is a more qualified name that can be used to
identify each entity? I would not consider that a hard problem, just an
annoyance. I read this as “if you deviate from the suggested scheme,
things might become a little bit less convenient, but everything still
works” which I find fair enough.
Dipl.-Math. Dipl.-Inform. Joachim Breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: This is a digitally signed message part
More information about the isabelle-dev