From f7ac27f54a76582354964bae21ee03937c108187 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 12 Jul 2024 22:01:57 +0200
Subject: Squashed commit of the following:

commit 7aeefe2e761a4892ff2f438e00f3ec7e6d286c5c
Author: Andreas Grois <andi@grois.info>
Date:   Fri Jul 12 21:59:44 2024 +0200

    Finish Lean 4.9 update.

commit 8a5576ae983203035f6bf0c807b36f1b4d7b63a6
Author: Andreas Grois <andi@grois.info>
Date:   Fri Jul 12 21:40:21 2024 +0200

    Lean 4.9 upgrade, heap is where it was before...

commit db34881e21391c96a6a0b939552b0f6f77d05bd8
Author: Andreas Grois <andi@grois.info>
Date:   Fri Jul 12 00:31:22 2024 +0200

    Further Lean 4.9 compat...

commit 22444613d58c5bd1a3fcdad0cd6c8d3aee1f3214
Author: Andreas Grois <andi@grois.info>
Date:   Thu Jul 11 22:15:11 2024 +0200

    Further Lean 4.9 porting

commit a4ace32cbb02959f9625578b511c2486e0816367
Author: Andreas Grois <andi@grois.info>
Date:   Wed Jul 10 23:18:29 2024 +0200

    Continue porting to Lean 4.9

commit d0f411bcc42b5cb7c72c2ed65ae35875c72e95dd
Author: Andreas Grois <andi@grois.info>
Date:   Wed Jul 10 23:10:34 2024 +0200

    Continue port to Lean 4.9

commit 835ce644b97840048de0df40676ff6f3a8b99985
Author: Andreas Grois <andi@grois.info>
Date:   Wed Jul 10 22:14:59 2024 +0200

    Partial port to Lean 4.9. Not compiling yet.
---
 Day8.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Day8.lean')

diff --git a/Day8.lean b/Day8.lean
index 229ca85..2f64247 100644
--- a/Day8.lean
+++ b/Day8.lean
@@ -109,7 +109,7 @@ private def part1_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints)
     | Except.error $ some n => part1_impl waypoints instructions remainingStarts n.fst n.snd
   else
     none -- walking in circles
-  termination_by part1_impl a b c d e => c.length
+  termination_by possibleStarts.length
 
 open Lean in
 def part1 (input : List Instruction × List Waypoint) : Option Nat :=
@@ -158,7 +158,7 @@ private def part2_impl (waypoints : Lean.HashMap WaypointId ConnectedWaypoints)
     | Except.error $ some n => part2_impl waypoints instructions n.fst remainingStarts n.snd
   else
     none -- walking in circles
-  termination_by part2_impl a b c d e => totalRemainingStarts d
+  termination_by totalRemainingStarts possibleStarts
 
 -- Okay, tried Brute Force, it did NOT work. Or rather, it might work, but I won't be able to prove
 -- termination for it. Not that it wouldn't be possible to prove, just I won't manage to.
@@ -280,7 +280,7 @@ private def findCyclingGoalsInPath_impl (waypoints : Lean.HashMap WaypointId Con
       some {start := n, interval := cycleLength : CyclingGoal}
     else
       none -- goal was reached before we started to walk in cycles, ignore.
-  termination_by findCyclingGoalsInPath_impl a b c d e f g => c.length
+  termination_by possibleStarts.length
 
 private def findCyclingGoalsInPath (waypoints : Lean.HashMap WaypointId ConnectedWaypoints) (instructions : List Instruction) (possibleStarts : List WaypointId) (startPosition : WaypointId) : List CyclingGoal :=
   findCyclingGoalsInPath_impl waypoints instructions possibleStarts [] [] startPosition 0
-- 
cgit v1.2.3

