Submission Details

Back to Submissions List

Challenge: filterIf

Submitted by: fogofchess

Submitted at: 2024-11-15 18:15:11

Code:

def filterIf(xs:List Int)(p:Int->Bool):List Int

List.filter p xs

First Theorem Proof:

theorem filterIf_correct(xs:List Int)(p:Int->Bool):
  filterIf xs p = List.filter p xs

rfl

Status: Incorrect

Feedback:

/tmp/tmpzkqyi60c/code.lean:6:0: error: unexpected end of input; expected ':=', 'where' or '|'
/tmp/tmpzkqyi60c/code.lean:4:39: error: function expected at
  List ℤ
term has type
  Type