summaryrefslogtreecommitdiff
path: root/Day8.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2025-10-12 18:44:32 +0200
committerAndreas Grois <andi@grois.info>2025-10-12 18:44:32 +0200
commit6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 (patch)
tree171a1a1b459b82f016e756e8649767a2d1311160 /Day8.lean
parent2a9261d1ba962deff9fcc1784be44563af513af5 (diff)
Lean 4.19
Diffstat (limited to 'Day8.lean')
-rw-r--r--Day8.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/Day8.lean b/Day8.lean
index 4e5d1bc..b4802f4 100644
--- a/Day8.lean
+++ b/Day8.lean
@@ -50,7 +50,7 @@ private def parseWaypoints (input : List String) : Except String $ List Waypoint
open Std in
private def validateWaypointLinks (waypoints : List Waypoint) : Bool :=
- let validLinks := HashSet.insertMany HashSet.empty $ waypoints.map Waypoint.id
+ let validLinks := HashSet.insertMany HashSet.emptyWithCapacity $ waypoints.map Waypoint.id
waypoints.all λw ↦ validLinks.contains w.left && validLinks.contains w.right
def target : WaypointId := "ZZZ"