Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: Violeta Hernández Palacios

Submitted at: 2024-11-19 09:01:01

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 

:= by ring

Status: Incorrect

Feedback:

Try this: ring_nf
/tmp/tmp1euqtt_o/proof.lean:8:3: error: unsolved goals
a b : ℤ
⊢ a + solveAdd a b = b