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

[Joachim Breitner]

Hi,

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:
> 
> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-July/001674.html

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.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130329/f898b102/attachment.sig>