Names with underscores

Stream: lean4

[Martin Dvořák]

In current naming conventions, are there places where names contain underscores?

I'm looking at https://leanprover.github.io/lean4/doc/lean3changes.html#style-changes for naming conventions; let me know if there is a better reference now.

[Jireh Loreaux]

Sure, theorems are still snake_cased, however, if they contain references to defs, which are lowerCamelCase, then the casing of those is preserved.

[James Gallicchio]

e.g. toList_append :)

[Jireh Loreaux]

Except things that live in Sort u, which are UpperCamelCased when they are declared.

[Jireh Loreaux]

See naming conventions

[Martin Dvořák]

I find it a bit unfortunate that naming conventions are currently in three places:
https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users#naming-conventions
https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention
https://leanprover.github.io/lean4/doc/lean3changes.html#style-changes

Does it make sense to update the last reference? Or rather replace the section with a link to the former?

[Jireh Loreaux]

It would be a bit strange for Lean 4 core to link to Mathlib 4 for reference on the naming conventions.

[Martin Dvořák]

Should we link them the other way around then? Or do we want to maintain separate documents for Lean 4 naming conventions and Mathlib4 naming conventions?

[Arthur Paulino]

Core itself seems to follow that convention. So maybe the naming convention should be there and mathlib would reference the original source of guidelines (it does seem to be the case that mathlib guidelines descend from core practices)

[Martin Dvořák]

For the naming in Lean 4 core, is https://leanprover.github.io/lean4/doc/lean3changes.html#style-changes the main document?