diff options
Diffstat (limited to 'Day8.lean')
| -rw-r--r-- | Day8.lean | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -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 |