From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Fri, 10 Oct 2025 00:30:19 +0200 Subject: Lean 4.18 --- Day8.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'Day8.lean') diff --git a/Day8.lean b/Day8.lean index 079e485..4e5d1bc 100644 --- a/Day8.lean +++ b/Day8.lean @@ -101,7 +101,7 @@ private def pass (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (alread private def part1_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (alreadyDoneSteps : Nat) (currentPosition : WaypointId) : Option Nat := let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition - if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy + if _ht: remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy let passResult := pass waypoints alreadyDoneSteps currentPosition instructions match passResult with | Except.ok n => some n @@ -110,6 +110,8 @@ private def part1_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) ( else none -- walking in circles termination_by possibleStarts.length + decreasing_by + exact _ht open Std in def part1 (input : List Instruction × List Waypoint) : Option Nat := @@ -266,7 +268,7 @@ private def findCyclingGoalsInPathPass (waypoints : Std.HashMap WaypointId Conne private def findCyclingGoalsInPath_impl (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (visitedGoals : List Nat) (visitedStarts : List (WaypointId × Nat)) (currentPosition : WaypointId) (currentSteps : Nat) : List CyclingGoal := let remainingStarts := possibleStarts.filter λs ↦ s != currentPosition - if remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy + if _ht: remainingStarts.length < possibleStarts.length then -- written this way to make termination_by easy let visitedStarts := (currentPosition, currentSteps) :: visitedStarts let passResult := findCyclingGoalsInPathPass waypoints currentSteps currentPosition instructions visitedGoals match passResult with @@ -281,6 +283,8 @@ private def findCyclingGoalsInPath_impl (waypoints : Std.HashMap WaypointId Conn else none -- goal was reached before we started to walk in cycles, ignore. termination_by possibleStarts.length + decreasing_by + exact _ht private def findCyclingGoalsInPath (waypoints : Std.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPosition : WaypointId) : List CyclingGoal := findCyclingGoalsInPath_impl waypoints instructions possibleStarts [] [] startPosition 0 -- cgit v1.2.3