Zulip Chat Archive

Stream: lean4

Topic: what naming scheme to use in mathlib4


view this post on Zulip Kenny Lau (Jan 08 2021 at 17:27):

/poll What should we use in mathlib4?
camelCase and PascalCase
snake_case

view this post on Zulip Kenny Lau (Jan 08 2021 at 17:32):

Sebastian Ullrich said:

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

^
image.png

view this post on Zulip Heather Macbeth (Jan 08 2021 at 18:02):

What happens to the distinction between docs#group and docs#Group, from category theory?

view this post on Zulip Adam Topaz (Jan 08 2021 at 18:13):

If we end up using unification hints this wouldn't be an issue, right?

view this post on Zulip Adam Topaz (Jan 08 2021 at 18:17):

(assuming categories are still defined using classes, that is)

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2021 at 18:20):

Sorry, can you explain further? (Maybe I need to read more about unification hints.)

view this post on Zulip Adam Topaz (Jan 08 2021 at 18:45):

I don't really know what I'm talking about, but I remember monoids being declared in Leo's talk as M : Monoid

view this post on Zulip Adam Topaz (Jan 08 2021 at 18:45):

Maybe I misremembered


Last updated: May 18 2021 at 23:14 UTC