Lean 4.25feature/day17

1 files changed, 1 insertions, 1 deletions

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."