Submission Details

Back to Submissions List

Challenge: filterIf

Submitted by: fogofchess

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

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
:= by rfl

Status: Correct

Feedback: