[isabelle] Overriding reason not to use single quote or camelcase in identifiers?
I try not to ask these simple questions when I know so little, but I'd
need to ask this eventually. It's better to ask now, than later with a
couple thousand lines of code.
I've read the style guide in implementation.pdf, so I've read and seen
that the preferred identifier naming scheme uses the underscore
character "_". However, I don't like how it looks, but a bigger issue is
that I have to escape it in Latex. Right now, I'm not using the Isabelle
I'm kind of settling on a combination of limited camelcase use, and
using the single quote character, ( ' ), to separate words in an identifier.
For example, I have the identifer "emS'is'unique". Below, I include a
very fledgling theory where I don't know what I'm doing. It's to show
some of my identifier naming.
I haven't seen any naming like "emS'is'unique". Is this just a matter of
preference, or would doing a lot of that come back to haunt me? I'm
assuming if I don't get errors in jEdit when doing that kind of thing,
it's not going to come back to haunt me.
(I haven't figured out if the unicode characters in an email like this
show up correctly in other's email readers.)
(*sT....The set type.*)
(*scP...Axiom schema of comprehension property.*)
type_synonym scP = "sT ⇒ bool"
(*inS...Set membership predicate.*)
inS:: "sT ⇒ sT ⇒ bool" and
(*emS...The empty set.*)
(*emE...The empty set is empty.*)
emE: "∀a::sT. ¬(inS a emS)" and
(*upS...Unordered pair set.*)
upS: "∀(a::sT)(b::sT). (∃c::sT. ∀x. (inS x c) ⟷ (x = a) ∨ (x = b))" and
(*scS...Schema set: axiom schema of comprehension.*)
scS: "∀(a::sT)(P::scP). (∃b::sT. ∀x. (inS x b) ⟷ ((inS x a) ∧ (P x)))"
(*Meaningless. It's merely a result of names.*)
theorem emS'unique'meaningless : "(a = emS) ∧ (b = emS) ⟹ a = b"
theorem emS'is'unique: "a = emS ⟷ (∀x::sT. ¬(inS x a))"
This archive was generated by a fusion of
Pipermail (Mailman edition) and