set.any

Stream: Is there code for X?

[Patrick Thomas]

Is there a function that takes a finite set and returns a boolean indicating whether any of the elements in that set satisfy a predicate function?

[Ruben Van de Velde]

Maybe you could start with finset.filter and go from there, of there's nothing better

[Patrick Thomas]

Thank you.

[Yaël Dillies]

(finset.filter s p).nonempty is what you want. You will need decidable equality and decidability of p.

[Patrick Thomas]

Thank you.

[Eric Wieser]

Can you just directly use ∃ x ∈ s, p x?

[Patrick Thomas]

I think it needs to be a computable function that can be used with if then else.

[Yaël Dillies]

∃ x ∈ s, p x is decidable if s is a finset. No need to reinvent the wheel.

[Patrick Thomas]

I can use that in ite?

[Patrick Thomas]

I'll give it a try. Thank you.