Zulip Chat Archive

Stream: Is there code for X?

Topic: Classical Choice on `finset`

Marcus Rossel (Jan 15 2021 at 21:24):

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

Adam Topaz (Jan 15 2021 at 21:26):

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

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

Yakov Pechersky (Jan 15 2021 at 21:28):

Yes, you can. docs#finset.choose

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.

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.

Adam Topaz (Jan 15 2021 at 21:32):

gotcha.

Last updated: Dec 20 2023 at 11:08 UTC