From 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 12 Oct 2025 18:44:32 +0200
Subject: Lean 4.19

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

(limited to 'Day15.lean')

diff --git a/Day15.lean b/Day15.lean
index cf2629d..4490223 100644
--- a/Day15.lean
+++ b/Day15.lean
@@ -65,8 +65,8 @@ private structure HolidayAsciiStringHelperManualArrangementProcedure (α β : Ty
 
 private def HolidayAsciiStringHelperManualArrangementProcedure.empty (α β : Type) : HolidayAsciiStringHelperManualArrangementProcedure α β :=
   {
-    boxes := Array.mkArray UInt8.size [],
-    valid := Array.size_mkArray _ _
+    boxes := Array.replicate UInt8.size [],
+    valid := Array.size_replicate
   }
 
 private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (data : β) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β :=
@@ -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 index.isLt).substr old.valid
+    valid := (Array.size_set 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 index.isLt).substr old.valid
+    valid := (Array.size_set index.isLt).substr old.valid
   }
 where
   tryRemove (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) :=
-- 
cgit v1.2.3

