summaryrefslogtreecommitdiff
path: root/Day3.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2024-12-17 19:47:14 +0100
committerAndreas Grois <andi@grois.info>2024-12-17 19:47:14 +0100
commit19d4b4e41a967c0c8b3329cd1c4a0617178c5a94 (patch)
treee5aff19158c526ebf5fbec2b51c8cde9da8e129f /Day3.lean
parent8f1a6c619a238531aed9dd3f4479d658fcf1d101 (diff)
Lean 4.14
Diffstat (limited to 'Day3.lean')
-rw-r--r--Day3.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/Day3.lean b/Day3.lean
index fd6fbc8..00ef709 100644
--- a/Day3.lean
+++ b/Day3.lean
@@ -103,7 +103,7 @@ def part2 (schematic : Schematic) : Nat :=
-- because here we need quick lookup for the numbers, not the parts.
open Std(HashMap) in
let numberCoordinates : HashMap Coordinate PartNumber :=
- HashMap.ofList $ schematic.numbers.bind $ λ pn ↦ pn.positions.map (·, pn)
+ HashMap.ofList $ schematic.numbers.flatMap $ λ pn ↦ pn.positions.map (·, pn)
let gearSymbols := schematic.parts.filter (Part.symbol · == '*')
-- but the symbols aren't enough, they need to be adjacent to **exactly** 2 numbers
let numbersNextGearSymbols := List.eraseReps <$> gearSymbols.map λgs ↦