Sean Leather (Apr 26 2018 at 09:40):
@Chris Hughes updated his
finset.disjoint PR with a change to rename the following:
Personally, I prefer the new names: they are more descriptive and don't rely on positional naming, which can be confusing. But I wanted to open up a discussion on this in general to determine the mathlib style guidelines. I don't think these types of things have been consistently named.
Sean Leather (Apr 26 2018 at 09:42):
We probably want feedback from @Johannes Hölzl and @Mario Carneiro in particular.
Chris Hughes (Apr 26 2018 at 16:06):
There's also the question of which one's
right and which one's
left. I would have named
dvd_mul_right : a ∣ a * b
Kenny Lau (Apr 26 2018 at 16:59):
@Chris Hughes confer or.inl and or.inr
Sean Leather (Apr 30 2018 at 06:44):
I created a GitHub issue for this discussion. Please leave any thoughts there.
Last updated: May 06 2021 at 18:20 UTC