diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/Nat.lean | 3 | ||||
| -rw-r--r-- | Common/Parsing.lean | 11 |
2 files changed, 14 insertions, 0 deletions
diff --git a/Common/Nat.lean b/Common/Nat.lean index 3a605a9..9d0ee29 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -20,3 +20,6 @@ theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) := match b with | 0 => h₁ | _ + 1 => /-(Nat.pred_succ a).substr $-/ Nat.lt_succ_of_lt h₁ + +theorem lt_imp_pred_lt {a b : Nat} (h₁ : a < b) : (a.pred < b) := + Nat.lt_of_le_of_lt (Nat.pred_le a) h₁ 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}" |