Largest element satisfying P in range

Stream: Is there code for X?

[Stuart Presnell]

I know that at least one element in range e satisfies a predicate P. How do I find the largest element in range e satisfying P?

[Yaël Dillies]

How do you know there exists a largest one?

[Yaël Dillies]

Do you mean docs#finset.range? If so, then use docs#nat.find_greatest.

[Junyan Xu]

I would use docs#finset.filter + docs#finset.max'