28

Author: TwoFX

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'
 ```
--/
+-/