Re: [isabelle] What naming will cause potential errors?
On Sun, 7 Apr 2013, Gottfried Barrow wrote:
If possible, I'd like to know what naming conventions I "have to" follow
to prevent future, potential errors due to naming.
There is nothing you "have to" follow. Naming conventions are a matter to
keep things simple at very little cost -- they belong to "best practices".
Observing certain customs routinely saves a lot of energy to rethink and
reconsider things over and over again. Sometimes this has to be done,
nonethrless: e.g. for Isabelle/Scala I've re-used many Isabelle/ML
conventions at the cost of violating other conventions on the Java Virtual
Machine, and Scala itself tends towards very mixed ways of writing. I had
to spend extra time to study history, manuals, websites to ensure that no
bad consequences are coming from Graph.is_minimal in both Isabelle/ML and
Isabelle/Scala, and not Graph.is_minimal here and Graph.isMinimal there
Anyway, the mail thread you mention was initiated by the surprise that
using a lower-case theory name in Isabelle/HOL makes the Haskell code
generator fail due to resulting lower-case module name, which Haskell
Theory names in Isabelle have a long-standing naming tradition: capital
words (usually in singular), separated by underscore.
Example (good): Vector_Space.
Counter-examples (bad): Vector_Spaces, VectorSpaces, vectorSpaces,
Many years ago, theory names were als very short, since users had to
repeat typing use_thy invocations a lot on the TTY, but has changed a lot
with the introduction of Proof General in 1998. Today there is nothing
special saying outright what you mean with theory Boolean_Algebra, which
former generations would have squeezed that towards 8 or 5 characters.
The majority of material within a theory body uses lower case names (also
separate by underscore). Some special situation have capitalized or
all-caps names, e.g. "max", "Max", "MAX" for certain families of
Locale names are within a theory body, and thus lower-case.
locale vector_space = ...
definition "foo = ..."
This produces fully qualified names like
with name space accesses like
Vector_Space.foo -- "global access"
vector_space.foo -- "local access"
That is the basic observation from 1999, when locales were first
introduced. Further complexity has piled up since then, but the basic
advantage of having access to two important hierary levels is still there
-- by convention, not by special machinery that would introduce extra
You do get overlaps in certain more complex cases nonetheless, but the
convention is somewhat better off than doing it just arbitrarily.
This archive was generated by a fusion of
Pipermail (Mailman edition) and