How to convert finset N to list N

Stream: new members

[Rui Liu]

Given s: finset N, I want to get a list of sorted values, how do I do that? I tried s.sort nat.lt but that doesn't work.

[Adam Topaz]

I think there's a docs#finset.to_list ?

[Eric Wieser]

I think it was more an exists_list

[Kevin Buzzard]

There's docs#finset.sort

[Adam Topaz]

I guess F.1.1 or something like that should spit out some list

[Rob Lewis]

You need to sort by a total relation, try nat.le. Best written as

import data.finset
example (s : finset ℕ) : list ℕ := s.sort (≤)

[Adam Topaz]

where F is a finset

[Rui Liu]

Oh shit, nat.le works whereas nat.lt doesn't work? Why is that so?

[Kevin Buzzard]

If you look at the docs it says it wants a total order

[Adam Topaz]

There's also a docs#multiset.to_list so you can do F.1.to_list

[Kevin Buzzard]

you can just click through to see the definitions. is_total means docs#is_total which is true for \le but not \lt

[Rui Liu]

Oh, since we don't have x < x in both direction, < is not a total order, whereas <= is!

[Rui Liu]

Thanks!

[Kevin Buzzard]

Right

[Adam Topaz]

(Oh, I just read that you wanted it sorted, sorry! If you don't care about sorting for some reason, you can convert to a multiset then to a list.)