From 4848d2516919ab7e5652b20e2b33e7cc39a9d4d9 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Thu, 28 Nov 2024 21:53:47 +0100 Subject: Day 14, Part 1. --- Common/Parsing.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'Common/Parsing.lean') diff --git a/Common/Parsing.lean b/Common/Parsing.lean index 3c5887a..c811319 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -47,6 +47,17 @@ def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coor instance : GetElem (RectangularGrid Element) (RectangularGrid.Coordinate grid) Element (λg _ ↦ g = grid) where getElem := λ g c h ↦ g.Get (h▸c) +def RectangularGrid.set {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : RectangularGrid Element := + let index := (Fin.cast grid.size_valid.symm coordinate.toIndex) + { + grid with + elements := grid.elements.set index value + size_valid := (grid.elements.size_set index value).substr grid.size_valid + } + +theorem RectangularGrid.set_same_size {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : (grid.set coordinate value).width = grid.width ∧ (grid.set coordinate value).height = grid.height := + ⟨rfl,rfl⟩ + instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where toString := λe ↦ Id.run do let mut r := s!"Width: {e.width}, Height: {e.height}" -- cgit v1.2.3