## Stream: Is there code for X?

### Topic: decidable search on a list

#### Bhavik Mehta (Jul 19 2020 at 15:51):

instance (f : α → Prop) (l : list α) [decidable_pred f] : decidable (∃ a, a ∈ l ∧ f a) :=
begin

end


How can I get this to work without going classical? (In case this is #xy, my actual case is in defining an algorithm where I want to get something from the list if there is one, and doing nothing if there isn't one)

#### Kenny Lau (Jul 19 2020 at 15:52):

have you tried moving the membership to the existential clause?

#### Bhavik Mehta (Jul 19 2020 at 15:52):

that works but then when I try to use it, list.choose gets confused

#### Kenny Lau (Jul 19 2020 at 15:54):

well you can destruct the existential when providing the proof for list.choose

#### Bhavik Mehta (Jul 19 2020 at 15:54):

But this is a different problem so that works, thanks!

Last updated: May 07 2021 at 22:14 UTC