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