GitHub failed
Proof body (as submitted)
theorem not_answer (n : Nat) : n + 0 = n := Nat.add_zero n
proof_body_hash:
f299ae7f1f1f943754570c09dc432c0379647c0d3cca7a8446d4b1c7085615d9Generated Lean file
What the judge actually compiles
-- AUTO-GENERATED by Leanforces. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgy91u80001yrvvnde7ph60
import Leanforces.Challenges.C0001.Statement
import Mathlib
namespace Leanforces.Challenges.C0001.Submissions.Submission_cmpgy91u80001yrvvnde7ph60
-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
theorem not_answer (n : Nat) : n + 0 = n := Nat.add_zero n
-- └── USER SUBMISSION BODY END ────────────────────────────
/-- App-appended type check. Refuses to compile unless
`answer` has type `∀ (n : Nat), n + 0 = n`. -/
def solution_target : ∀ (n : Nat), n + 0 = n := answer
#print axioms solution_target
end Leanforces.Challenges.C0001.Submissions.Submission_cmpgy91u80001yrvvnde7ph60
file_hash (recomputed):
cca97c5f54148bd6b3b6018144b0231986f0dd14e97c5ac31cba8f7ac81a234b ✗ DOES NOT match stored hashGitHub
Branchsubmission/cmpgy91u80001yrvvnde7ph60
Commit SHAddaa373f3ba4b6dba5e80169f597fa0b61bb1b9f
PR #—