From 8d6efb1c1fdddc1fbad167510ce25e56be684130 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
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
---
 Day2.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Day2.lean')

diff --git a/Day2.lean b/Day2.lean
index 7208a3d..7ed10aa 100644
--- a/Day2.lean
+++ b/Day2.lean
@@ -78,7 +78,7 @@ def part2 (games : List Game) : Nat :=
 
 open DayPart
 instance : Parse ⟨2, by simp⟩ (ι := List Game) where
-  parse := parse
+  parse := (λ o ↦ match o with | some a => pure a | none => throw "Failed to parse input") ∘ parse
 
 instance : Part ⟨2,_⟩ Parts.One (ι := List Game) (ρ := Nat) where
   run := some ∘ part1
-- 
cgit v1.2.3