Zulip Chat Archive

Stream: mathlib4

Topic: Bounded vs BddAbove

Yury G. Kudryashov (Sep 17 2023 at 22:06):

We have docs#Set.Bounded, docs#BddAbove, and docs#BddBelow. Should we reuse the former for the other two?

Yaël Dillies (Sep 18 2023 at 05:17):

No. Violeta Hernández added (a lot of API for) the former because she didn't know about the latter two, but in general we prefer predicates specialised to <=, >= for usability.

Yury G. Kudryashov (Sep 18 2023 at 14:41):

Should we drop the former then?

Yury G. Kudryashov (Sep 18 2023 at 14:42):

Or at least mention BddAbove/BddBelow in the docstring?

Yaël Dillies (Sep 18 2023 at 14:43):

What are the current uses of Set.Bounded? In principle, I'm happy to drop it.

Yury G. Kudryashov (Sep 19 2023 at 00:59):

It is used in Order/Bounded (a lot), in Order/RelClasses (def + 2 lemmas), Order/WellFounded (2 lemmas), Cardinal/Cofinality (2 theorems), and Ordinal/Arithmetic (once).

Yury G. Kudryashov (Sep 19 2023 at 01:00):

Do you know that Lean 4 extension can show all uses of a definition/lemma?

Yury G. Kudryashov (Sep 19 2023 at 01:00):

(not hidden ones like in by simp)

Alex J. Best (Sep 19 2023 at 01:03):

You can right click and click on "Find all references"

Yaël Dillies (Sep 19 2023 at 06:12):

Ah no I didn't!

Last updated: Dec 20 2023 at 11:08 UTC