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

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

(limited to 'Day16.lean')

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
   }
-- 
cgit v1.2.3