From 8223584095273bc7bdf7b7dc65a6e168350cdf57 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sat, 14 Dec 2024 00:09:46 +0100
Subject: Begin Day16

---
 Common/Parsing.lean | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Common/Parsing.lean')

diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index c811319..348db25 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -21,6 +21,12 @@ structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where
   x : Fin grid.width
   y : Fin grid.height
 
+instance {grid : RectangularGrid Element} : BEq grid.Coordinate where
+  beq := λa b ↦ a.x == b.x && a.y == b.y
+
+instance {grid : RectangularGrid Element} : Hashable grid.Coordinate where
+  hash := λa ↦ Hashable.hash (a.x, a.y)
+
 instance : ToString (RectangularGrid.Coordinate grid) where
   toString := λx ↦ s!"x: {x.x}/{grid.width}, y : {x.y}/{grid.height}"
 
-- 
cgit v1.2.3

