Submission Details

Back to Submissions List

Challenge: solveSub

Submitted by: GasStationManager

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

Code:

import Init.Data.Int

def solveSub(a b:Int): Int

:=a-b

First Theorem Proof:

theorem solveSub_correct(a b:Int): a - (solveSub a b)=b

:=simp[solveSub]

Status: Incorrect

Feedback:

/tmp/tmpbwi_8vlj/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