Lean 4.19

1 files changed, 2 insertions, 2 deletions

diff --git a/Day16.lean b/Day16.lean
index 8bd4bf8..abefc51 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -197,9 +197,9 @@ private def SeenExitDirections.empty (table : OpticsTable) : SeenExitDirections
   {
     width := table.width
     height := table.height
-    elements := Array.mkArray (table.width * table.height) default
+    elements := Array.replicate (table.width * table.height) default
     not_empty := table.not_empty
-    size_valid := Array.size_mkArray _ _
+    size_valid := Array.size_replicate
     sameHeight := rfl
     sameWidth := rfl
   }