From b37fc3089eb0ca8fc37a82ae6d6071b0accbca19 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sat, 21 Dec 2024 21:37:51 +0100
Subject: Continue Day17

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

(limited to 'Common/Parsing.lean')

diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 637f807..ebc5589 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -24,6 +24,18 @@ structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where
 instance {grid : RectangularGrid Element} : BEq grid.Coordinate where
   beq := λa b ↦ a.x == b.x && a.y == b.y
 
+instance {grid : RectangularGrid Element} : LawfulBEq grid.Coordinate where
+  rfl := λ{a} ↦ by
+    unfold BEq.beq instBEqCoordinate
+    simp only [beq_self_eq_true, Bool.and_self]
+  eq_of_beq := λ{a b} h₁ ↦ by
+    unfold BEq.beq instBEqCoordinate at h₁
+    simp only [Bool.and_eq_true, beq_iff_eq] at h₁
+    cases a
+    cases b
+    simp at h₁ ⊢
+    assumption
+
 instance {grid : RectangularGrid Element} : Hashable grid.Coordinate where
   hash := λa ↦ Hashable.hash (a.x, a.y)
 
-- 
cgit v1.2.3

