From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 10 Oct 2025 00:30:19 +0200
Subject: Lean 4.18

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

(limited to 'Day15.lean')

diff --git a/Day15.lean b/Day15.lean
index 5158910..cf2629d 100644
--- a/Day15.lean
+++ b/Day15.lean
@@ -71,7 +71,7 @@ private def HolidayAsciiStringHelperManualArrangementProcedure.empty (α β : Ty
 
 private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (data : β) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β :=
   let h := HolidayAsciiStringHelperAble.holidayAsciiStringHelper label
-  let index := Fin.cast old.valid.symm h.val
+  let index := Fin.cast old.valid.symm h.toFin
   let box := old.boxes[index]
   let box := updateOrAppend box []
   {
@@ -90,7 +90,7 @@ where
 
 private def HolidayAsciiStringHelperManualArrangementProcedure.remove {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β :=
   let h := HolidayAsciiStringHelperAble.holidayAsciiStringHelper label
-  let index := Fin.cast old.valid.symm h.val
+  let index := Fin.cast old.valid.symm h.toFin
   let box := old.boxes[index]
   let box := tryRemove box []
   {
-- 
cgit v1.2.3

