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
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