what naming scheme to use in mathlib4

Stream: lean4

[Kenny Lau]

/poll What should we use in mathlib4?
camelCase and PascalCase
snake_case

[Kenny Lau]

Sebastian Ullrich said:

Patrick Massot said:

I would say we should follow Lean + core lib with definitions, but keep underscores in lemma names.

FWIW, that's what I suggested last year image.png

^
image.png

[Heather Macbeth]

What happens to the distinction between docs#group and docs#Group, from category theory?

[Adam Topaz]

If we end up using unification hints this wouldn't be an issue, right?

[Adam Topaz]

(assuming categories are still defined using classes, that is)

[Bryan Gin-ge Chen]

Sorry, can you explain further? (Maybe I need to read more about unification hints.)

[Adam Topaz]

I don't really know what I'm talking about, but I remember monoids being declared in Leo's talk as M : Monoid

[Adam Topaz]

Maybe I misremembered

[Michael Jam]

Looking at List.Mem theorems in Init.Data.List.Basic, I find the naming convention slightly confusing. https://leanprover-community.github.io/mathlib4_docs////Init/Data/List/Basic.html#List.Mem
Mem starts with a capital letter but the following lemmas are List.mem_... instead of List.Mem_...
Does it mean I should uncapitalize or snakify Mem in a theorem name? I am unsure what to do and I find that weird to do.

List.Mem could be defined with a recursive def instead of an inductive. But inductive Prop's are preferred because it makes proofs easier.
However it sounds inelegant to decide to write Mem instead of mem just because that particular Prop happens to be recursively defined.

My suggestion is probably naive but wouldn't it be cleaner to change the naming conventions for something like:
any declaration ending with a Prop, or with Prop: like_that (connectives should be in lower case)
defs (not Props, not theorems): likeThat
inductive types (not Props): LikeThat
?

[David Renshaw]

My understanding is roughly: defs, namespaces, structures get capital camelcase. Theorems and lemmas get snake_case.

[David Renshaw]

Current conventions are codified by mathport, and you can see its latest output here: https://github.com/leanprover-community/lean3port/blob/f2dc09b58e3e976fb99eab9c5f2b659a27e2dc2a/Leanbin/Init/Data/List/Basic.lean#L46

[David Renshaw]

(Ignore the little ₓ.)

[Michael Jam]

OK I wasn't aware that def's that end with Sort are LikeThat. I thought a def was a term name in Sebastian's convention. I guess it's motivated by the idea that namespaces created by Props should always be capitalized. I kind of dislike that convention but that's only my taste..