Submission Details

Back to Submissions List

Challenge: mapInt

Submitted by: eric-wieser

Submitted at: 2024-11-15 11:36:20

Code:

def mapInt(xs:List Int)(f:Int->Int):List Int

[] /-

First Theorem Proof:

theorem mapInt_correct(xs:List Int)(f:Int->Int)
: (mapInt xs f).length=xs.length
∧  ∀ i:Fin xs.length, (mapInt xs f)[i]! = f xs[i]

-/

Status: Incorrect

Feedback:

/tmp/tmpacgbn8dl/code.lean:6:0: error: unterminated comment
/tmp/tmpacgbn8dl/code.lean:4:36: error: function expected at
  List ℤ
term has type
  Type
/tmp/tmpacgbn8dl/code.lean:4:0: error: declaration body is missing