diff options
Diffstat (limited to 'Common/Parsing.lean')
| -rw-r--r-- | Common/Parsing.lean | 12 |
1 files changed, 12 insertions, 0 deletions
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) |