From 4784df61d4858f9f470327e46822aabf2f7eff52 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 1 Dec 2024 19:58:11 +0100 Subject: Minor, indentation --- Day15.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Day15.lean') diff --git a/Day15.lean b/Day15.lean index 92bcbc2..bb7a01c 100644 --- a/Day15.lean +++ b/Day15.lean @@ -117,7 +117,7 @@ private def focussingPower (hashMap : HolidayAsciiStringHelperManualArrangementP (λ(totalPower, lensIndex) lens ↦ (totalPower + boxIndex * lensIndex * lens.snd.val, lensIndex + 1)) (totalPower, 1) (totalPower, boxIndex + 1) - ) + ) (0,1) private instance : HolidayAsciiStringHelperAble Substring where -- cgit v1.2.3