From 83215dd16965d9c3e6545dcad52df9a4912c7cc0 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 25 Mar 2026 06:38:28 +0000
Subject: [PATCH] 66

---
 HumanEvalLean/HumanEval66.lean | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval66.lean b/HumanEvalLean/HumanEval66.lean
index f873697..1e71103 100644
--- a/HumanEvalLean/HumanEval66.lean
+++ b/HumanEvalLean/HumanEval66.lean
@@ -1,7 +1,30 @@
 module
 
-def digitSum : Unit :=
-  ()
+def digitSum (s : String) : Nat :=
+  s.chars.filter Char.isUpper
+    |>.map Char.toNat
+    |>.fold (init := 0) (· + ·)
+
+example : digitSum "" = 0 := by cbv
+example : digitSum "abAB" = 131 := by cbv
+example : digitSum "abcCd" = 67 := by cbv
+example : digitSum "helloE" = 69 := by cbv
+example : digitSum "woArBld" = 131 := by cbv
+example : digitSum "aAaaaXa" = 153 := by cbv
+
+theorem digitSum_eq {s : String} :
+    digitSum s = ((s.toList.filter Char.isUpper).map Char.toNat).sum := by
+  simp [digitSum, ← Std.Iter.foldl_toList, List.sum_eq_foldl]
+
+theorem digitSum_empty : digitSum "" = 0 := by simp [digitSum_eq]
+
+theorem digitSum_push_of_isUpper {s : String} {c : Char} (h : c.isUpper = true) :
+    digitSum (s.push c) = digitSum s + c.toNat := by
+  simp [digitSum_eq, List.filter_cons_of_pos h]
+
+theorem digitSum_push_of_isUpper_eq_false {s : String} {c : Char} (h : c.isUpper = false) :
+    digitSum (s.push c) = digitSum s := by
+  simp [digitSum_eq, List.filter_cons_of_neg (Bool.not_eq_true _ ▸ h)]
 
 /-!
 ## Prompt
@@ -50,4 +73,4 @@ def check(candidate):
     assert candidate("You arE Very Smart") == 327, "Error"
 
 ```
--/
\ No newline at end of file
+-/