From 770d7c86652a2b812c1d44f7e7bb500832a5fa45 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 07:58:53 +0000
Subject: [PATCH] 29

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

diff --git a/HumanEvalLean/HumanEval29.lean b/HumanEvalLean/HumanEval29.lean
index cf497bf..6217399 100644
--- a/HumanEvalLean/HumanEval29.lean
+++ b/HumanEvalLean/HumanEval29.lean
@@ -1,7 +1,12 @@
 module
 
-def filter_by_prefix : Unit :=
-  ()
+def filterByPrefix (l : List String) (pref : String) : List String :=
+  l.filter (·.startsWith pref)
+
+open Classical in
+theorem filterByPrefix_eq {l : List String} {pref : String} :
+    filterByPrefix l pref = l.filter (fun s => pref.toList <+: s.toList) := by
+  simp [filterByPrefix, ← String.startsWith_string_iff]
 
 /-!
 ## Prompt
@@ -40,4 +45,4 @@ def check(candidate):
     assert candidate([], 'john') == []
     assert candidate(['xxx', 'asd', 'xxy', 'john doe', 'xxxAAA', 'xxx'], 'xxx') == ['xxx', 'xxxAAA', 'xxx']
 ```
--/
\ No newline at end of file
+-/