From 3a9ff92902df508074daa3017d1a71dae7e85248 Mon Sep 17 00:00:00 2001 From: Andreas Grois 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