Zulip Chat Archive

Stream: Is there code for X?

Topic: decidable search on a list


view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 19 2020 at 15:52):

have you tried moving the membership to the existential clause?

view this post on Zulip Bhavik Mehta (Jul 19 2020 at 15:52):

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

view this post on Zulip Kenny Lau (Jul 19 2020 at 15:54):

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

view this post on Zulip 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