From 671ccf18e506398fd8eb65ebac92ec6d2fd03ccd Mon Sep 17 00:00:00 2001 From: Andreas Grois 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