Re: [isabelle] What naming will cause potential errors?

On 4/12/2013 4:10 PM, Makarius wrote:
I did not invent these conventions, but I do think that lower-case is better for the mass of text. Note that I normally don't argue about the ease of *writing* the sources, since ease of *reading* has the prime priority. This is why the underscore is important to separate words, and lower-case helps the Western brain to gloss quickly over large bodies of text (this is why the scribes of Charlemagne invented the miniscules). Uppercase still has its role in situations of special emphasis, e.g. "max", "Max", "MAX", but it would loose that benefit if it were used by default.

Your statement, "Note that I normally don't argue about the ease of *writing* the sources, since ease of *reading* has the prime priority", is usefully quotable. For one to be opinionated about a topic can many times result in one being perceived as presumptuous, whereas one being opinionated about the same topic, while also providing a quote from someone with good, establishment credentials, can, instead, result in putting others on the defense.

I had already "primarily" adopted your non-use of camel case, but the other half to readability is the line length of code, and standard mathematical notation demonstrates how much information you can get on one line, where, other than the graphical symbols, it's mainly because of the use of single letters, or single subscripted letters.

I do, though, use a little bit of camel case, so today, I've made me a rule about that. The rule is that I only use camel case to separate characters or cryptic sequences of characters, or characters acting as a prefix or suffix to words.

For example, I'm naming my operators like inP, ssO, eqO, xeO, geU, geI, and so forth. And then I also have a name for the same operators with names something like P\<^isub>I\<^isub>n, where part of the reasoning of both styles of names is to try and prevent global names clashes with the HOL sources, and what names other people are using. My use of a name P\<^isub>I\<^isub>n then requires sometimes that a theorem name will start with P\<^isub>I\<^isub>n.

What I've said about my naming is still tied into my original question for this thread. First, I want to know what the rules are (which you've already answered). It's best to stay with community convention if breaking convention will cause problems down the road.


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