findIf

write a function that, given a List of integers and a predicate function p that takes an integer and returns a boolean, returns an element of the list x if p x = true. If such x does not exist, return none

Function Signature

def findIf(xs:List Int)(p:Int->Bool):Option Int

Theorem Signature

theorem findIf_some(xs:List Int)(p:Int->Bool):
  (∃ x∈ xs, p x) -> ∃ y∈ xs, findIf xs p=some y ∧ p y

Additional Theorem Signature

theorem findIf_none(xs:List Int)(p:Int->Bool):
  (¬ ∃ y∈ xs, p y =true)-> findIf xs p=none 

View All Submissions

Please log in or register to submit a solution for this challenge.