diff options
Diffstat (limited to 'Day15.lean')
| -rw-r--r-- | Day15.lean | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 [] { |
