Lean 4.18

1 files changed, 2 insertions, 2 deletions

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 []
   {