diff options
Diffstat (limited to 'Day5.lean')
| -rw-r--r-- | Day5.lean | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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} |