inconsistent spelling (capitalization): goal, Lemma

noschinl / cyp

Checker for "morally correct" induction proofs about haskell programs

MIT License

29 stars 10 forks source link

inconsistent spelling (capitalization): goal, Lemma #17

Open jwaldmann opened 7 years ago

jwaldmann commented 7 years ago

in theory texts, lower case: axiom, goal.
in proof texts: upper case: Lemma, Proof, QED, IH
... and lower case: def

I find upper case very inconvenient for typing (needs one more key). Does it improve readability? Not sure. "QED" definitely feels overdone. (Or is this because Latin didn't have lower case letters at all?)

How does Isabelle do it - all keywords start with lowercase letter?

larsrh commented 7 years ago

Yes, keywords are all lowercase. Sometimes things get all caps identifiers, e.g. in Isabelle/ML code.

larsrh commented 7 years ago

We could switch to a lowercase convention in cyp too. I don't feel strongly about it.