Zulip Chat Archive

Stream: new members

Topic: How to convert finset N to list N


view this post on Zulip Rui Liu (Dec 09 2020 at 23:20):

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.

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:20):

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

view this post on Zulip Eric Wieser (Dec 09 2020 at 23:21):

I think it was more an exists_list

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 23:21):

There's docs#finset.sort

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:23):

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

view this post on Zulip Rob Lewis (Dec 09 2020 at 23:23):

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

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

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:23):

where F is a finset

view this post on Zulip Rui Liu (Dec 09 2020 at 23:24):

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

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 23:24):

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

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:25):

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

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 23:25):

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

view this post on Zulip Rui Liu (Dec 09 2020 at 23:26):

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

view this post on Zulip Rui Liu (Dec 09 2020 at 23:26):

Thanks!

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 23:27):

Right

view this post on Zulip Adam Topaz (Dec 09 2020 at 23:28):

(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.)


Last updated: May 11 2021 at 13:22 UTC