Zulip Chat Archive

Stream: general

Topic: naming of `Prop` instances

Eric Rodriguez (Jul 18 2021 at 12:04):

is there any particular reason that boolean_algebra Prop is named boolean_algebra_Prop instead of Prop.boolean_algebra? (the auto-given name is sort.<instance>, which is something I'm fixing right now and why I noticed)

Eric Rodriguez (Jul 19 2021 at 11:02):

/poll

Eric Rodriguez (Jul 19 2021 at 11:03):

okay, so there's now a PR for this to change the default heuristic in Lean3 source. Does anyone have any preference on what instances should be named?

Mario Carneiro (Jul 19 2021 at 11:22):

I would prefer for it not to be fixed in the source. There are only like 2 of these and they make lean more complicated

Eric Rodriguez (Jul 19 2021 at 11:24):

#8360 is the mathlib PR for this

Eric Wieser (Jul 23 2021 at 11:21):

Unless anyone else votes on the poll above, I'll merge #8360 as-is with Prop. / Type. as the chosen spelling. We can always change lean itself later if we decide to.

Last updated: Dec 20 2023 at 11:08 UTC