Accepted🌱 +5 Seeds awarded
Proof body (as submitted)
lemma helper (n : Nat) : n + 0 = n := Nat.add_zero n theorem answer (n : Nat) : n + 0 = n := helper n
proof_body_hash:
8909d528b93d0b1a39e75c3e6558558920a60747b01020c8ea2070a2b54f0a5aGenerated Lean file
What the judge actually compiles
-- AUTO-GENERATED by ProofGarden Lean Judge. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgy89ff00019ge4qa0lxyh2
import ProofGarden.Challenges.C0001.Statement
import Mathlib
namespace ProofGarden.Challenges.C0001.Submissions.Submission_cmpgy89ff00019ge4qa0lxyh2
-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
lemma helper (n : Nat) : n + 0 = n := Nat.add_zero n
theorem answer (n : Nat) : n + 0 = n := helper 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 ProofGarden.Challenges.C0001.Submissions.Submission_cmpgy89ff00019ge4qa0lxyh2
file_hash (recomputed):
05d7ee322b66d8014a6cdf100806f4b1f9ccf6e244b5bac79ff123bc43f9406c ✓ matches stored hashGitHub
Branchsubmission/cmpgy89ff00019ge4qa0lxyh2
Commit SHA1d6e421fbe965ed063d52760a1fccc71764d350f
PR #—