Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: Kevin Buzzard

Submitted at: 2024-11-15 11:28:15

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

import Mathlib
def solveAdd (a b:Int): Int := b - a

First Theorem Proof:

theorem solveAdd_correct (a b: Int): a + (solveAdd a b) =b 

theorem solveAdd_correct (a b: Int): a + (solveAdd a b) =b := by unfold solveAdd; exact?

Status: Incorrect

Feedback:

/tmp/tmp4fnkj1kz/code.lean:4:27: error: unexpected token 'import'; expected ':=', 'where' or '|'
/tmp/tmp4fnkj1kz/code.lean:5:0: error: invalid 'import' command, it must be used in the beginning of the file