From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001 From: Andreas Grois 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