From b37fc3089eb0ca8fc37a82ae6d6071b0accbca19 Mon Sep 17 00:00:00 2001 From: Andreas Grois 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