sort finsets

Stream: new members

[Simon Daniel]

Hi,
is it possible to sort a finset by the Ord typeclass?
It does not seem to play well with finsets, i tried

inductive I | A | B | C
deriving  Fintype, Ord

def sorted: List I := (Fintype.elems).sort (Ord.compare) -- sort expects I -> I -> Prop
def sorted2: List I := (Fintype.elems).sort (λ x y => Ord.compare x y = Ordering.lt)
-- cannot derive IsTrans IsAntisymm IsTotal

if not by Ord, is there another solution without manual definition of an ordering?

[Albus Dompeldorius]

I think you want a LinearOrder. Then you can do Fintype.elems.sort (· ≤ ·).

[Eric Wieser]

Unfortunately I don't think deriving LinearOrder currently works, but it would be a good project to make it do so