Zulip Chat Archive

Stream: Is there code for X?

Topic: every finite type admits a linear order

Johan Commelin (Apr 21 2022 at 18:10):

Surely this is somewhere, but I couldn't find it...

Yaël Dillies (Apr 21 2022 at 18:11):

What do you want exactly? Extending an existing order or declaring an arbitrary one? Neither of those is tied to finiteness.

Johan Commelin (Apr 21 2022 at 18:12):

Just a random linear order

Yaël Dillies (Apr 21 2022 at 18:12):

docs#well_ordering_rel

Johan Commelin (Apr 21 2022 at 18:12):

And yes, I guess I don't need finiteness

Reid Barton (Apr 21 2022 at 18:13):

& docs#is_well_order.linear_order

Eric Rodriguez (Apr 21 2022 at 18:14):

Reid Barton said:

& docs#is_well_order.linear_order

i'm guessing this isn't turned on by default for diamond/constructivist reasons, right?

Yaël Dillies (Apr 21 2022 at 18:14):

It wouldn't even make sense for it to be an instance because r is free.

Eric Rodriguez (Apr 21 2022 at 18:15):

ah right, derp

Johan Commelin (Apr 21 2022 at 18:16):

Thanks! My problem is solved :grinning:

Last updated: Dec 20 2023 at 11:08 UTC