From db75b31132f03dd8246f8ac010282f92d2eed40e Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 07:31:46 +0000
Subject: [PATCH 1/2] 28

---
 HumanEvalLean/HumanEval28.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval28.lean b/HumanEvalLean/HumanEval28.lean
index 8f84ff6..c9bf985 100644
--- a/HumanEvalLean/HumanEval28.lean
+++ b/HumanEvalLean/HumanEval28.lean
@@ -1,7 +1,12 @@
 module
 
-def concatenate : Unit :=
-  ()
+def concatenate (strings : List String) : String :=
+  String.join strings
+
+theorem toList_concatenate {strings : List String} :
+    (concatenate strings).toList = strings.flatMap String.toList := by
+  -- https://github.com/leanprover/lean4/pull/13091
+  simp [concatenate]
 
 /-!
 ## Prompt
@@ -41,4 +46,4 @@ def check(candidate):
     assert candidate(['x', 'y', 'z']) == 'xyz'
     assert candidate(['x', 'y', 'z', 'w', 'k']) == 'xyzwk'
 ```
--/
\ No newline at end of file
+-/

From 3e60c008581f39acf73c28d4facb248cf7f24102 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Thu, 26 Mar 2026 08:20:20 +0000
Subject: [PATCH 2/2] Fix

---
 HumanEvalLean/HumanEval28.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/HumanEvalLean/HumanEval28.lean b/HumanEvalLean/HumanEval28.lean
index c9bf985..970e9ce 100644
--- a/HumanEvalLean/HumanEval28.lean
+++ b/HumanEvalLean/HumanEval28.lean
@@ -5,7 +5,6 @@ def concatenate (strings : List String) : String :=
 
 theorem toList_concatenate {strings : List String} :
     (concatenate strings).toList = strings.flatMap String.toList := by
-  -- https://github.com/leanprover/lean4/pull/13091
   simp [concatenate]
 
 /-!