Re: [isabelle] Variables in locale assumptions
On Fri, 21 Feb 2014, bnord wrote:
Am 21.02.2014 18:33, schrieb Makarius:
Note that "Test" is a bad name for a locale: lower-case is normally used.
Likewise, theory names are usually capitalized words (in singular),
separated by underscore. (You did not show that in the example, but I
guess > 50% that you've had a lowercase test.thy here, or was it just
Do you know anything about the intended audience for his development
that you think the "default" Isabelle style is appropriate for him? Or
is it just the objectively "best" style?
Locales in capitals and theories in lower-case probably stems from Java
(classes vs. packages), but the world is bigger than Java.
The objectively best style for Isabelle is the one devised by the people
who implemented qualified name spaces and locales, type classes and more
over the years. By observing the very simple scheme of Theory.locale.item
or Theory.class.item, you get more robust name space accesses for free
(there is no cost to follow a simple convention).
Just a few days ago, I have mentally revisited the situation for qualified
theory names (by the session name, which is also capitalized), and
completion in the Prover IDE for all these names. So that is still
relevant, even though people tend to become forgetful. Maybe I should
make the Prover IDE inform the user about naming conventions, just to save
time explaining them again and again.
This archive was generated by a fusion of
Pipermail (Mailman edition) and