From 2390fe0a2fbbdd283d21049a1e997026d7d1948c Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 7 Jan 2025 23:32:53 +0100
Subject: Lean 4.15

---
 Day15.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Day15.lean')

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 (α × β) :=
-- 
cgit v1.2.3

