From 671ccf18e506398fd8eb65ebac92ec6d2fd03ccd Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 13 Apr 2025 20:43:15 +0200
Subject: Lean 4.17

---
 Day7.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Day7.lean')

diff --git a/Day7.lean b/Day7.lean
index 218e643..04c55f7 100644
--- a/Day7.lean
+++ b/Day7.lean
@@ -119,8 +119,8 @@ def parse (input : String) : Except String (List Player) := do
 
 def part1 (players : List Player) : Nat :=
   players.quicksortBy (λ p q ↦ p.hand < q.hand)
-  |> List.enumFrom 1
-  |> List.foldl (λ r p ↦ p.fst * p.snd.bet + r) 0
+  |> (List.zipIdx · 1)
+  |> List.foldl (λ r p ↦ p.snd * p.fst.bet + r) 0
 
 
 ------------------------------------------------------------------------------------------------------
@@ -194,8 +194,8 @@ def part2 (players : List Player) : Nat :=
   let players := players.map λ p ↦
     {bet := p.bet, hand2 := p.hand.toHand2 : Player2}
   players.quicksortBy (λ p q ↦ p.hand2 < q.hand2)
-  |> List.enumFrom 1
-  |> List.foldl (λ r p ↦ p.fst * p.snd.bet + r) 0
+  |> (List.zipIdx · 1)
+  |> List.foldl (λ r p ↦ p.snd * p.fst.bet + r) 0
 
 ----------------------------------------------------------------------------------------------------
 open DayPart
-- 
cgit v1.2.3

