[isabelle] What naming will cause potential errors?


On the developer's list I saw some discussion about problems that naming can cause.

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 by that.

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 conventions.

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 MHonArc.