double-capital identifiers

Stream: mathlib4

[Kevin Buzzard]

Lean 4 has Prod and PProd. My understanding of the algorithm is that the Lean 3 lemma pprod_prod should become pProdProd. I'm wondering if pprodProd is better. We're not going to be writing lE_of_lT I guess...

[Mario Carneiro]

le_of_lt is handled in the current wording by saying that LE is an acronym, but that doesn't suffice for PProd which is not an acronym. I think it should be extended to say that the acronym-like casing rule should extend to definitions that start with an acronym prefix like ABCDefGhi, which gets lowercased to abcdefGhi.

[Kevin Buzzard]

Is there also an issue with things like MetaM which have capitals at the end?

[Mario Carneiro]

those would stay capitalized

[Mario Carneiro]

we already have functions like List.mapM so it doesn't look out of place

[Yakov Pechersky]

mathlib3 lemma pprod_prod I thought becomes mathlib4 thoerem PProd_Prod

[Mario Carneiro]

no, that's covered by https://github.com/leanprover-community/mathlib4/wiki#naming-convention

[Mario Carneiro]

Note that the original example that pprod_prod is a definition (of an Equiv), not a theorem. If it was a theorem, it would be named pprod_prod

[Mario Carneiro]

I've been contemplating whether we should allow things that are definitions but "morally" act like theorems to use the theorem naming convention (definitions of Equivs and category theory in particular come to mind). This gets awkward though because the fact that they are really defs shows up later when you want to prove coherence lemmas using them as name components