Submission Details

Back to Submissions List

Challenge: solveAdd0

Submitted by: GasStationManager

Submitted at: 2024-11-14 04:59:56

Code:

import Init.Data.Int

def solveAdd0(a:Int): Int

:= -a

First Theorem Proof:

theorem solveAdd0_correct(a: Int): a +(solveAdd0 a)=0

:= simp[solveAdd]

Status: Incorrect

Feedback:

/tmp/tmp6iim1tem/code.lean:2:0: error: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/root/.elan/toolchains/leanprover--lean4---v4.14.0-rc2/lib/lean