28 (#290)

Author: TwoFX

HumanEvalLean/HumanEval28.lean

@@ -1,7 +1,11 @@
 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
+  simp [concatenate]
 
 /-!
 ## Prompt
@@ -41,4 +45,4 @@ def check(candidate):
     assert candidate(['x', 'y', 'z']) == 'xyz'
     assert candidate(['x', 'y', 'z', 'w', 'k']) == 'xyzwk'
 ```
--/
+-/