Zulip Chat Archive

Stream: lean4

Topic: capitalization


view this post on Zulip Kenny Lau (Jan 07 2021 at 11:44):

When do we capitalize names?

view this post on Zulip Patrick Massot (Jan 07 2021 at 11:57):

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

view this post on Zulip Kenny Lau (Jan 07 2021 at 11:58):

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

view this post on Zulip Rob Lewis (Jan 07 2021 at 12:01):

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

view this post on Zulip Kenny Lau (Jan 07 2021 at 12:02):

I see

view this post on Zulip Rob Lewis (Jan 07 2021 at 12:03):

I forsee a lot of people accidentally coercing true to True

view this post on Zulip Sebastian Ullrich (Jan 07 2021 at 12:06):

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


Last updated: May 18 2021 at 23:14 UTC