From 3a9ff92902df508074daa3017d1a71dae7e85248 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 21:08:35 +0100
Subject: Lean 4.25

---
 Day4.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Day4.lean')

diff --git a/Day4.lean b/Day4.lean
index 4466053..27cb08b 100644
--- a/Day4.lean
+++ b/Day4.lean
@@ -38,7 +38,7 @@ def parse (input : String) : Except String Deck := do
         let winners := String.trim $ g[0]'(by simp[q])
         let draws := String.trim $ g[1]'(by simp[q])
         let toNumbers := λ(s : String) ↦
-          s.split (·.isWhitespace)
+          s.splitToList (·.isWhitespace)
           |> List.filter (not ∘ String.isEmpty)
           |> List.mapM String.toNat?
         let winners ← if let some winners := toNumbers winners then pure winners else throw "Failed to parse winning numbers."
-- 
cgit v1.2.3