Zulip Chat Archive

Stream: maths

Topic: naming of binary properties with left and right


view this post on Zulip Sean Leather (Apr 26 2018 at 09:40):

@Chris Hughes updated his finset.disjoint PR with a change to rename the following:

  • empty_disjointdisjoint_empty_left
  • disjoint_emptydisjoint_empty_right

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.

view this post on Zulip Sean Leather (Apr 26 2018 at 09:42):

We probably want feedback from @Johannes Hölzl and @Mario Carneiro in particular.

view this post on Zulip 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 dvd_mul_left

view this post on Zulip Kenny Lau (Apr 26 2018 at 16:59):

@Chris Hughes confer or.inl and or.inr

view this post on Zulip 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