Lean 4.15

5 files changed, 8 insertions, 8 deletions

diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index d68a313..91bb751 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -88,7 +88,7 @@ def RectangularGrid.set {grid : RectangularGrid Element} (coordinate : grid.Coor
   {
     grid with
       elements := grid.elements.set index value
-      size_valid := (grid.elements.size_set index value).substr grid.size_valid
+      size_valid := (grid.elements.size_set index value index.isLt).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 :=
diff --git a/Day15.lean b/Day15.lean
index bb7a01c..5158910 100644
--- a/Day15.lean
+++ b/Day15.lean
@@ -76,7 +76,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : T
   let box := updateOrAppend box []
   {
     boxes := old.boxes.set index box
-    valid := (Array.size_set old.boxes index box).substr old.valid
+    valid := (Array.size_set old.boxes index box index.isLt).substr old.valid
   }
 where
   updateOrAppend (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) :=
@@ -95,7 +95,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.remove {α β : T
   let box := tryRemove box []
   {
     boxes := old.boxes.set index box
-    valid := (Array.size_set old.boxes index box).substr old.valid
+    valid := (Array.size_set old.boxes index box index.isLt).substr old.valid
   }
 where
   tryRemove (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) :=
diff --git a/Day16.lean b/Day16.lean
index d91f6ad..ec602ca 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -226,7 +226,7 @@ private def SeenExitDirections.countExitDirections {table : OpticsTable} (seenDi
   let c := seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0
   have h₁ : c ≤ 4 * seenDirections.width * seenDirections.height := by
     have : c = seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0 := (rfl : c = seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0)
-    rw[this, Array.foldl_eq_foldl_toList]
+    rw[this, ←Array.foldl_toList]
     have : seenDirections.elements.toList.length = seenDirections.elements.size :=  Array.length_toList
     rw[seenDirections.size_valid] at this
     rw[Nat.mul_assoc,←this]
@@ -266,7 +266,7 @@ private theorem SeenExitDirections.countExitDirections_increasesWhenSet {table :
   simp at h₁ ⊢
   unfold Parsing.RectangularGrid.Coordinate.toIndex at h₁ ⊢
   unfold Array.set
-  simp[Array.foldl_eq_foldl_toList] at h₁ ⊢
+  simp[←Array.foldl_toList] at h₁ ⊢
   rw[Array.getElem_eq_getElem_toList] at h₁ ⊢
   apply countExitDirections_increasesWhenSet_Aux
   assumption
diff --git a/lakefile.lean b/lakefile.lean
index 3c764e1..ec4ca09 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -32,7 +32,7 @@ lean_exe «aoc-2023» where
   supportInterpreter := true
 
 require BinaryHeap from git
-  "https://github.com/soulsource/BinaryHeap"@"376e4bf573f754aa7cb8c5d6ed652f1efece3050"
+  "https://github.com/soulsource/BinaryHeap"@"fe30e1dc0a0070452edce74331aa3df21a6b8f7c"
 
 require «lean-astar» from git
-  "https://github.com/soulsource/lean-astar"@"3514e38cf48b611abc808b7de4c13862d3a4ede0"
+  "https://github.com/soulsource/lean-astar"@"4cc7ae8a6653402e091d246ed746a0ed45b099dc"
diff --git a/lean-toolchain b/lean-toolchain
index cb2924f..f1f4005 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.14
+leanprover/lean4:4.15.0