Zulip Chat Archive
Stream: general
Topic: ord_connected_subset_conditionally_complete_linear_order
Yury G. Kudryashov (Jan 12 2022 at 02:27):
Currently, this instance depends on [inhabited s]. Do you mind if I change it to [nonempty s]?
Yury G. Kudryashov (Jan 12 2022 at 02:30):
Pro: we drop a data dependency. Con: we no longer can prescribe a specific garbage value.
Yury G. Kudryashov (Jan 12 2022 at 02:44):
UPD: ignore, it's used for nnreals
Yury G. Kudryashov (Jan 12 2022 at 02:51):
Another question: what do you think about making this a non-instance like subtype.has_Sup / subtype.has_Inf?
Yury G. Kudryashov (Jan 12 2022 at 02:52):
I want to define set.Icc.complete_linear_order
Yury G. Kudryashov (Jan 12 2022 at 02:52):
And I can't do it with these has_Sup/has_Inf
Last updated: Dec 20 2023 at 11:08 UTC