Casing convention

Stream: lean4

[Marcus Rossel]

Has there been a final consensus on casing conventions?
I thought I'd read about it in some thread, but I can't find it anymore.
In particular, I'm interested in the conventions for the following items:

• Types (UpperCamelCase?)
• Non-type definitions (lowerCamelCase?)
• Theorems (something involving underscores?)

[Mac]

@Marcus Rossel you are on the right track. The current conventions (as I understand them) are:

• Things in Type/Sort: UpperCamelCase
• Normal definitions: lowerCamelCase
• Theorems/keywords: lower_snake_case

[Scott Morrison]

At some point we'll need to work out the convention for "Bundled things with a category instance", possibly SHOUTING. e.g. in Lean3 we had group vs Group. Now that group is Group, we need something new for the category of (bundled) groups. I'm not particularly keen on SHOUTING, but it is used in the literature. An alternative is to ask for more allowed characters in identifiers, and use 𝖦𝗋𝗈𝗎𝗉 (unicode san serif), but that has type-ability concerns!

[Mario Carneiro]

A simpler alternative that I have used in... other provers is GroupCat

[Kyle Miller]

\mathbf{Group} :upside_down:

If backslash were allowed in identifiers, \Group wouldn't be that crazy. (That's a combination of how I'd write it anyway in LaTeX and how apparently the Arend theorem prover uses backslashes to indicate keywords.) Edit: Oh right, that will play havoc with input for the Lean extensions for VS Code and Emacs...

[Gabriel Ebner]

𝕲𝖗𝖔𝖚𝖕 :smile:

[Kevin Buzzard]

I guess this is how the 19th century German greats wrote categories

[Marcus Rossel]

How would you handle this?:

structure EvenNat where
  n : Nat
  isEven : ...

or

structure EvenNat where
  n : Nat
  is_even : ...

[Mario Carneiro]

The ... is relevant. Assuming is_even is a proof of a proposition, it should be snake cased