Undocumented informal policy

Stream: mathlib4

[Michael Rothgang]

For the #mathlib4 > Refactoring idea den thread, I was wondering: is there any other undocumented informal policy coming to mind, which would be useful to write down? If you know one, please leave a comment in the thread!

[Michael Rothgang]

@Johan Commelin @Kim Morrison Perhaps one of you can forward this request within the maintainers as needed. (I don't want to ping everybody, but I am very grateful for any input.)

[Notification Bot]

A message was moved from this topic to #mathlib4 > Naming convention for structure projections and dot notation by Bhavik Mehta.

[Edward van de Meent]

some things that come to mind:

• american spelling
• when to use classical

[Kim Morrison]

Do we actually have even an informal policy on spelling?

While personally I'm happy, despite natively using Australian spelling, with deciding to use American, I think a better policy would be "either American or British is just fine, and please don't make edits switching between them".

[Eric Wieser]

The fact that initialize is a keyword is presumably a point towards preferring american spelling?

[Eric Wieser]

I guess we can always break disputes with things like nhds to avoid the question of whether there is a u

[Peter Nelson]

Sadly for graph theorists, clr isn’t so standard.

[Michael Rothgang]

I added both items to the idea list, thanks!

[Antoine Chambert-Loir]

Eric Wieser said:

I guess we can always break disputes with things like nhds to avoid the question of whether there is a u

See https://www.cbc.ca/news/canada/british-columbia/the-penthouse-marquee-hate-speech-allegation-1.7428625