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

---
 Day5.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Day5.lean')

diff --git a/Day5.lean b/Day5.lean
index 44c3908..27c69a6 100644
--- a/Day5.lean
+++ b/Day5.lean
@@ -110,7 +110,7 @@ structure Almanach where
 private def parseSeeds (input : String) : Except String (List Seed) :=
   if input.startsWith "seeds: " then
     let input := input.drop 7
-    let input := String.trim <$> input.split Char.isWhitespace
+    let input := String.trim <$> input.splitToList Char.isWhitespace
     let numbers := input.mapM String.toNat?
     let numbers := if let some numbers := numbers then pure numbers else throw s!"Failed to parse a seed number in {input}"
     List.map NatId.fromNat <$> numbers
@@ -118,7 +118,7 @@ private def parseSeeds (input : String) : Except String (List Seed) :=
     throw s!"Seeds line does not start with \"seeds: \": {input}"
 
 private def parseMapping {α β : Type} [NatId α] [NatId β] (input : String) : Except String $ Mapping α β := do
-  let input := String.trim <$> input.split Char.isWhitespace
+  let input := String.trim <$> input.splitToList Char.isWhitespace
   let nums ← input.mapM $ (λ o ↦ if let some o := o then pure o else throw s!"Failed to parse mapping {input}, expected number") ∘ String.toNat?
   match nums with
   | [a,b,c] => pure $ {inputStart := NatId.fromNat b, outputStart := NatId.fromNat a, length := c}
-- 
cgit v1.2.3

