capitalization

Stream: lean4

[Kenny Lau]

When do we capitalize names?

[Patrick Massot]

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

[Kenny Lau]

My question is inspired by the fact that True : Prop and true : Bool

[Rob Lewis]

I think types are UpperCamelCase and non-type terms are lowerCamelCase, right?

[Kenny Lau]

I see

[Rob Lewis]

I forsee a lot of people accidentally coercing true to True

[Sebastian Ullrich]

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