Zulip Chat Archive

Stream: Is there code for X?

Topic: Classical Choice on `finset`


view this post on Zulip Marcus Rossel (Jan 15 2021 at 21:24):

Is it possible to somehow choose an item from a finset à la classical.choice?

view this post on Zulip Adam Topaz (Jan 15 2021 at 21:26):

You need nonempty. The empty set is still finite :)

view this post on Zulip Adam Topaz (Jan 15 2021 at 21:27):

What do you mean by choose? Are you in the middle of a tactic block? If so, you can do a case-split using docs#finset.nonempty

view this post on Zulip Yakov Pechersky (Jan 15 2021 at 21:28):

Yes, you can. docs#finset.choose

view this post on Zulip Yakov Pechersky (Jan 15 2021 at 21:29):

You have provide a proof that the element you'll be choosing is in the finset, and moreover, the unique one satisfying the property you're choosing for.

view this post on Zulip Marcus Rossel (Jan 15 2021 at 21:30):

Adam Topaz said:

What do you mean by choose? Are you in the middle of a tactic block? If so, you can do a case-split using docs#finset.nonempty

I mean extract some element from the set. So nonempty is exactly what I need for that.

view this post on Zulip Adam Topaz (Jan 15 2021 at 21:32):

gotcha.


Last updated: May 07 2021 at 22:14 UTC