From 11639a915b229952c267deb03a367ef70bb4a27e Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 1 Dec 2024 19:57:39 +0100
Subject: Change Day15 Part 2 to not use do-notation.

---
 Day15.lean | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/Day15.lean b/Day15.lean
index c04d854..92bcbc2 100644
--- a/Day15.lean
+++ b/Day15.lean
@@ -109,14 +109,16 @@ where
 
 /- Funny, by the way, that the riddle only needs insert/remove, but not find... -/
 
-private def focussingPower (hashMap : HolidayAsciiStringHelperManualArrangementProcedure Substring (Fin 10)) : Nat := Id.run do
-  let mut totalPower := 0
-  for h : boxIndex in [:hashMap.boxes.size] do
-    let mut lensIndex := 0
-    for lens in hashMap.boxes[boxIndex] do
-      lensIndex := lensIndex + 1
-      totalPower := totalPower + (1 + boxIndex) * lensIndex * lens.snd.val
-  totalPower
+private def focussingPower (hashMap : HolidayAsciiStringHelperManualArrangementProcedure Substring (Fin 10)) : Nat :=
+  Prod.fst $
+  hashMap.boxes.foldl (
+    λ(totalPower, boxIndex) box ↦
+      let totalPower := Prod.fst $ box.foldl
+        (λ(totalPower, lensIndex) lens ↦ (totalPower + boxIndex * lensIndex * lens.snd.val, lensIndex + 1))
+        (totalPower, 1)
+      (totalPower, boxIndex + 1)
+      )
+    (0,1)
 
 private instance : HolidayAsciiStringHelperAble Substring where
   holidayAsciiStringHelper := holidayAsciiStringHelper 0
-- 
cgit v1.2.3