From 0f4a1836c5dde5bbc5b2ced20ba1c5fb75b0347c Mon Sep 17 00:00:00 2001
From: Alessandro Sosso <alesosso@gmail.com>
Date: Sat, 28 Mar 2026 15:20:25 +0100
Subject: [PATCH] changed format of provided spec in human_eval/problem_2

---
 src/lean4/human_eval/problem_2.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/lean4/human_eval/problem_2.lean b/src/lean4/human_eval/problem_2.lean
index cd021b0..3185ef3 100644
--- a/src/lean4/human_eval/problem_2.lean
+++ b/src/lean4/human_eval/problem_2.lean
@@ -23,14 +23,14 @@ def problem_spec
 (number: Rat) :=
 -- spec
 let spec (res) :=
+number > 0 →
 0 ≤ res ∧
 res < 1 ∧
 number.floor + res = number;
-number > 0 →
 -- program terminates
-(∃ result, impl number = result ∧
+∃ result, impl number = result ∧
 -- return value satisfies spec
-spec result)
+spec result
 -- end_def problem_spec
 
 -- start_def generated_spec