total order

Stream: Is there code for X?

[Aniruddh Agarwal]

Are total orders defined in mathlib?

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

guessing the name of something is surprisingly powerful

[Aniruddh Agarwal]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

they end up being defined in the same file

[Jalex Stark]

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]

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

[Mario Carneiro]

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]

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

[Yury G. Kudryashov]

AFAIR there is a class is_total

[Kenny Lau]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

You can use it to avoid declaring one more typeclass.

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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