Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: Command Master

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

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

b - a

First Theorem Proof:

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

unfold solveAdd
omega

Status: Incorrect

Feedback:

/tmp/tmporh8aedl/code.lean:6:0: error: unexpected end of input; expected ':=', 'where' or '|'
/tmp/tmporh8aedl/code.lean:4:24: error: function expected at
  ℤ
term has type
  Type