diff options
| author | Andreas Grois <andi@grois.info> | 2025-10-10 00:30:19 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-10-10 00:30:19 +0200 |
| commit | 2a9261d1ba962deff9fcc1784be44563af513af5 (patch) | |
| tree | e6c805e970924027723a159aa751e9aa0269ce7b /Day8.lean | |
| parent | 671ccf18e506398fd8eb65ebac92ec6d2fd03ccd (diff) | |
Lean 4.18
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 |