Zulip Chat Archive

Stream: general

Topic: as_linear_order

Yaël Dillies (Oct 05 2021 at 21:42):

Is there any point in keeping docs#as_linear_order around? Seems like this is a relique from an ancient time. You can always just fill in the fields of linear_order that are missing from partial_order, right?

Yury G. Kudryashov (Oct 05 2021 at 21:55):

But it's not convenient to do this in the middle of a proof.

Yaël Dillies (Oct 05 2021 at 21:55):

Is it ever used?

Yury G. Kudryashov (Oct 05 2021 at 21:56):

I don't know. Git grep

Last updated: Dec 20 2023 at 11:08 UTC