summaryrefslogtreecommitdiff
path: root/Day15.lean
diff options
context:
space:
mode:
Diffstat (limited to 'Day15.lean')
-rw-r--r--Day15.lean4
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 []
{