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