From 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 12 Oct 2025 18:44:32 +0200
Subject: Lean 4.19

---
 Day8.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Day8.lean')

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"
-- 
cgit v1.2.3