WellOrder class abbrev

Stream: mathlib4

[Violeta Hernández]

Is there any possibility we could make a WellOrder class abbrev for LinearOrder + WellFoundedLT?

[Violeta Hernández]

I feel like this structure is really common, but simultaneously it's not obvious that this is the "correct" way to write it

[Violeta Hernández]

Using docs#IsWellOrder often ends up being a bit of a footgun, for all the reasons we don't usually use unbundled relations

[Violeta Hernández]

I remember that there was some discussion about using the class abbrev feature but I don't remember if that came to a clear conclusion

[Jireh Loreaux]

I think it's really not that common in most of mathematics. You just happen to work on set theory, where it gets used a lot. That being said, I am open to being wrong here.

[Violeta Hernández]

Fair enough, "really common" is relative

[Violeta Hernández]

There's definitely a bunch of places where this gets used, though

[Violeta Hernández]

Are class abbrevs something we're fine with using liberally? Or would this have to be a really common typeclass for it to make sense?

[Violeta Hernández]

Or actually, is there any policy on class abbrevs to begin with?

[Jireh Loreaux]

I think we avoid class abbrev almost everywhere because it creates instances in both directions, and we suspect that would be bad for performance. At least, I believe @Eric Wieser thinks so.

[Eric Wieser]

We could try using it for something prominent like NonUnitalAlgebra and see what the cost is

[Eric Wieser]

But yes, my impression is that "Lean 4 can handle typeclass loops" is a simplification that doesn't apply to some of mathlib's more-dependent typeclasses