Lean 4.25feature/day17

1 files changed, 2 insertions, 2 deletions

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}