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
 Scratch.thy?)

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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.