Zulip Chat Archive

Stream: lean4

Topic: capitalization

Kenny Lau (Jan 07 2021 at 11:44):

When do we capitalize names?

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.

Kenny Lau (Jan 07 2021 at 11:58):

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

Rob Lewis (Jan 07 2021 at 12:01):

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

Kenny Lau (Jan 07 2021 at 12:02):

I see

Rob Lewis (Jan 07 2021 at 12:03):

I forsee a lot of people accidentally coercing true to True

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

Tesla Zhang (Jun 02 2024 at 05:06):

What is the rationale behind using PascalCase? I'm curious

Martin Dvořák (Jun 03 2024 at 17:16):

Distinguishing types from "normal" terms?

Last updated: May 02 2025 at 03:31 UTC