diff options
| author | Andreas Grois <andi@grois.info> | 2024-12-14 00:09:46 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-12-14 00:09:46 +0100 |
| commit | 8223584095273bc7bdf7b7dc65a6e168350cdf57 (patch) | |
| tree | 2934a22693564082e78d896d98769e0ddc0e9996 /Common/Parsing.lean | |
| parent | 4784df61d4858f9f470327e46822aabf2f7eff52 (diff) | |
Begin Day16
Diffstat (limited to 'Common/Parsing.lean')
| -rw-r--r-- | Common/Parsing.lean | 6 |
1 files changed, 6 insertions, 0 deletions
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}" |