From 4848d2516919ab7e5652b20e2b33e7cc39a9d4d9 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
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

