Re: [isabelle] locales and 'types'
On Tue, 13 Jul 2010, Peter Gammie wrote:
I find this reasoning a bit confusing for "types" as 'a cannot be used
in the RHS anyway, i.e. this is illegal too:
locale X =
fixes a :: "'a"
types Type = "'a set"
It is not a construct that copes with things that are already fixed in a
You can consider this limitation as an accidental feature of the current
implementation. Trying a bit harder in the internal structures, one could
support type parameters on the RHS one day. It is a very important
principle to base a system on assumptions that are as weak as possible, to
leave room for continued unfolding of the concepts behind it. Exploiting
the inability for type parameters on the RHS now would limit the future
growth of the system.
One more note on the example above. In order to avoid unnecessary
confusion and unexpected problems, it is important to stick to
established Isabelle naming conventions:
* Theory names: capitalized words, typically describing the main
in singular, e.g. "theory Foo_Bar_Concept"
* Almost everything else in lower case, especially locale and type
* Exceptions: capitalized datatype constructors, also some term
constructions according to typical mathematical usage (e.g. capital
singleton letters A, B, C, or occasional Foo for "sets" etc.)
Could I humbly suggest that these and other style rules be put in a
document that accompanies the distribution?
I promise to mention something like that in the next tutorial on Isar that
should come forward this year.
On the other hand we have a bit too many manuals that are often in an
inconsistent state, while many things that I find myself explaining again
and again are written in the "reference manuals" collection -- these 3 are
in fact mostly up to date: isar-ref, implementation, system.
Maybe the next generation of user interfaces needs to tell users directly
about thing that are better avoided, or point to relevant sections of the
manuals via formal references in the text.
This archive was generated by a fusion of
Pipermail (Mailman edition) and