[isabelle] What naming will cause potential errors?
On the developer's list I saw some discussion about problems that naming
If possible, I'd like to know what naming conventions I "have to" follow
to prevent future, potential errors due to naming.
I looked at the implementation manual:
Naming conventions for ML are spelled out some on page 3, "0.1.2 Naming
conventions". I'm not using ML, so I'm only concerned with Isar naming,
and it wasn't obvious to me that any hard rules exists, such as in
section "Names", page 46.
I'll take two specific cases, theory names and theorem names.
I was naming my theory with lowercase first letter. I have now changed
the first letter to uppercase, since it's a minor thing, and I have this
hunch that somewhere, there's a need for fully qualified names to abide
For theorem names, I name many theorems starting with uppercase, which
seems to be contrary to the convention in the HOL sources.
I have good reason to do this, because I care more about following
mathematical notation conventions than following Isabelle coding
However, if someone tells me that my naming scheme will potentially
cause errors, rather than just annoy people, I am more than ready to
give preference to any naming convention that "must be" followed to
prevent potential errors.
But I don't want to change my naming scheme without knowing what the
rules are because there are lots of different objects, in particular, in
addition to theorem names, there are locales, classes, and sublocales,
which I see that I may need now.
Can anyone tell me what Isar naming conventions "must be" followed to
prevent potential errors?
This archive was generated by a fusion of
Pipermail (Mailman edition) and