Submission Details

Back to Submissions List

Challenge: solveAdd0

Submitted by: GasStationManager

Submitted at: 2024-11-24 07:05:21

Code:

import Init.Data.Int

def solveAdd0(a:Int): Int

:=sorry

First Theorem Proof:

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

:=sorry

Status: Incorrect

Feedback:

Compilation error for /tmp/tmptrhl36rl/target.lean:
input file '/tmp/tmptrhl36rl/target.lean' must be contained in root directory (/root/CodeProofTheArena/)