Stream: Is there code for X?

Topic: total order

Aniruddh Agarwal (May 16 2020 at 02:19):

Are total orders defined in mathlib?

Jalex Stark (May 16 2020 at 02:24):

you might want to read init/algebra/order.lean

Jalex Stark (May 16 2020 at 02:25):

or you could just type linear_order. and look through the autocomplete suggestions to learn what stuff is associated with it

Jalex Stark (May 16 2020 at 02:25):

guessing the name of something is surprisingly powerful

Aniruddh Agarwal (May 16 2020 at 02:25):

Ah it's called linear_order, but I was searching for total_order

Jalex Stark (May 16 2020 at 02:26):

yes, when you're learning to search for things by name, you should try the tactic of putting in synonyms

Jalex Stark (May 16 2020 at 02:26):

although in some domains, we have strict naming conventions that make synonyms irrelevant

Jalex Stark (May 16 2020 at 02:27):

a different path to find linear_order might have been to start with partial orders

Jalex Stark (May 16 2020 at 02:27):

they end up being defined in the same file

Jalex Stark (May 16 2020 at 02:28):

you can do #print notation ≤ to learn there is a typeclass called has_le, and following up on that teaches you things how orders are defined

Jalex Stark (May 16 2020 at 02:28):

(asking questions on here is a great strategy, I'm just trying to give you strategies that might resolve even faster)

Mario Carneiro (May 16 2020 at 02:28):

You could also use library_search to find x <= y \/ y <= x, discover the name le_total, then look at the typeclass argument for it and see it's called linear_order

Mario Carneiro (May 16 2020 at 02:28):

or you could ask here and get an answer in seconds :)

Yury G. Kudryashov (May 16 2020 at 02:51):

AFAIR there is a class is_total

Kenny Lau (May 16 2020 at 06:51):

yeah but we don't use those is_ typeclasses and I don't know why they exist

Yury G. Kudryashov (May 16 2020 at 08:48):

E.g., we have a lemma assuming [semilattice_sup α] [is_total ((≤) : α → α → Prop)].

Yury G. Kudryashov (May 16 2020 at 08:48):

You can use it to avoid declaring one more typeclass.

Yury G. Kudryashov (May 16 2020 at 08:52):

BTW, do we ever have [semilattice sup α] [is_total (≤)] without a decidable_linear_order α?

Kevin Buzzard (May 16 2020 at 08:55):

The is_ classes are sometimes useful. But back to the point, the idea is that you should be able to search the docs for total order and the linear_order file should have this as a tag

Bryan Gin-ge Chen (May 16 2020 at 14:39):

The new fact technique lets us create new classes like the is_ classes too, right? Or is there a difference I'm missing.

Last updated: May 17 2021 at 16:26 UTC