Zulip Chat Archive

Stream: general

Topic: bounded.mono

Violeta Hernández (Jan 21 2022 at 19:14):

In a recent PR of mine, I unwittingly introduced a name clash between bounded.mono and metric.bounded.mono. I made issue #11589 for this, but I was told nobody reads those, so I'm asking here.

What would be the best course of action? Currently the alternatives I'm considering are putting bounded in the order namespace, and protecting metric.bounded.mono.

Yaël Dillies (Jan 21 2022 at 19:32):

For balance, the order namespace is barely used. I only know of docs#order.ideal

Bhavik Mehta (Jan 21 2022 at 20:07):

Can you put bounded in the set namespace, so we can write s.bounded r, and then bounded.mono can be written as set.bounded.mono?

Violeta Hernández (Jan 21 2022 at 20:15):

I really like that proposal!

Yaël Dillies (Jan 21 2022 at 20:20):

Oh yeah, of course! That would be best.

Yaël Dillies (Jan 21 2022 at 20:22):

However, metric.bounded could itself have been set.bounded, so we should write a little disambiguation note in the docstring.

Violeta Hernández (Jan 21 2022 at 22:58):

https://github.com/leanprover-community/mathlib/pull/11594

Yury G. Kudryashov (Jan 23 2022 at 17:09):

Should we use bounded for bdd_above/bdd_below?

Last updated: Dec 20 2023 at 11:08 UTC