From 8d6efb1c1fdddc1fbad167510ce25e56be684130 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Thu, 7 Dec 2023 20:26:51 +0100 Subject: Allow error messages in parsing (for debugging) And fix an off-by-one in day 5 --- Day1.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Day1.lean') diff --git a/Day1.lean b/Day1.lean index f0e9c14..d9f0c69 100644 --- a/Day1.lean +++ b/Day1.lean @@ -2,8 +2,8 @@ import Common namespace Day1 -def parse (input : String) : Option $ List String := - some $ input.split Char.isWhitespace |> List.filter (not ∘ String.isEmpty) +def parse (input : String) : List String := + input.split Char.isWhitespace |> List.filter (not ∘ String.isEmpty) -- Both parts could still be improved by doing two searches, one from the left, one from the right @@ -62,7 +62,7 @@ def part2 (instructions : List String) : Option Nat := open DayPart instance : Parse ⟨1, by simp⟩ (ι := List String) where - parse := parse + parse := pure ∘ parse instance : Part ⟨1, _⟩ Parts.One (ι := List String) (ρ := Nat) where run := part1 -- cgit v1.2.3