How to find instances

Stream: mathlib4

[Heather Macbeth]

Are there docs for std4 or core? In particular, I'd like to know how to find the instances of a class, which is something I would do in mathlib3 by finding the class in the docs and clicking "Instances of this typeclass".

#xy Has a Trans instance for < been implemented yet?

[Mario Carneiro]

#synth answers the xy problem

[Mario Carneiro]

docs4#Trans - maybe?

[Mario Carneiro]

Yes, that list includes mathlib4 instances

[Mario Carneiro]

so the answer to your question is no, it only exists over Nat not a Preorder

[Mario Carneiro]

basically, mathlib4 doc-gen already includes all of core + std4

[Heather Macbeth]

Thanks, #synth and the core + std4 coverage of the mathlib4 docs were both new to me.

I'll add the Trans instance for docs4#Preorder; should it live in the same file (Init.Algebra.Order) as Preorder itself?

What about the class docs4#Std.TransCmp? Should it also have a Trans instance?

[Heather Macbeth]

(PS: why does std have this separate order hierarchy?)

[Mario Carneiro]

The TransCmp class is intended specifically for the Std data structures; it could have a Trans instance for cmpLe but is not intended to be general purpose

[Mario Carneiro]

I'm still on the fence about whether we can move Preorder / PartialOrder / LinearOrder to std4, similar to what we had in lean 3 core. It would really restrict the number of imports it can have

[Mario Carneiro]

maybe things are better after @Scott Morrison 's refactor of the algebraic hierarchy, or maybe it needs another refactor, but it is easier to invent a separate hierarchy on the side than import portions of the official one along with half of mathlib