Submission Details

Back to Submissions List

Challenge: solveAdd0

Submitted by: kvanvels

Submitted at: 2024-11-15 17:00:40

Code:

import Init.Data.Int

def solveAdd0(a:Int): Int

:= -a

First Theorem Proof:

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

:= by
  unfold solveAdd0
  exact add_right_neg a

Status: Correct

Feedback:

/tmp/tmp86pge0q2/proof.lean:10:8: warning: `add_right_neg` has been deprecated, use `add_neg_cancel` instead