Lean 4.19

1 files changed, 4 insertions, 4 deletions

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 (α × β) :=