arbitrary linear order

Stream: Is there code for X?

[Yaël Dillies]

So we have encodable.fintype.encodable to put an arbitrary encodable instance on a fintype. Is there a similar thing to put a linear_order on any type?

[Yaël Dillies]

Actually, I only need antisymmetry and totality. My point is that I'm defining a pair of elements (a' b') = f a b for each pair of distinct elements (a, b), but I want f b a = (b', a') (f b a = (a', b') is fine too): I want to get the same witnesses from both sides. So one solution would be to order a and b before getting the witnesses.

[Bhavik Mehta]

docs#linear_extension lets you embed any partial order (in particular the trivial one) into an arbitrary linear order, which works for your first question; though we should be able to generate a well-order on any type but I can't seem to find that in mathlib any more

[Bhavik Mehta]

Ah, found it! docs#well_ordering_rel