Submission Details

Back to Submissions List

Challenge: mapInt

Submitted by: Kevin Buzzard

Submitted at: 2024-11-15 11:38:46

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]

:= by
  have oops : False := nomatch (rfl : Nat.ble 0 0 = true) ▸ (by native_decide : Nat.ble 0 0 = false)
  exact oops.elim

Status: Correct

Feedback:

/tmp/tmpjgxa7md9/proof.lean:4:11: warning: unused variable `xs`
note: this linter can be disabled with `set_option linter.unusedVariables false`
/tmp/tmpjgxa7md9/proof.lean:4:24: warning: unused variable `f`
note: this linter can be disabled with `set_option linter.unusedVariables false`