diff options
| -rw-r--r-- | Day10.lean | 4 | ||||
| -rw-r--r-- | Day16.lean | 2 | ||||
| -rw-r--r-- | Day7.lean | 8 | ||||
| -rw-r--r-- | lakefile.lean | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
5 files changed, 10 insertions, 10 deletions
@@ -1017,7 +1017,7 @@ private def noSolution {area : Area} : (List $ Area.PathHead area) → Bool section ListMonad local instance : Monad List where - bind := List.flatMap + bind := flip List.flatMap pure := List.singleton def part1 (area : Area) : List Nat := do @@ -1470,7 +1470,7 @@ section ListMonad -- We can do this here without perf issues. The list in question will never have more than 2 elements. local instance : Monad List where pure := List.singleton - bind := List.flatMap + bind := flip List.flatMap private inductive WestEastFoldState (area : Area) | inside : Coordinate area.width area.height → WestEastFoldState area @@ -267,7 +267,7 @@ private theorem SeenExitDirections.countExitDirections_increasesWhenSet {table : unfold Parsing.RectangularGrid.Coordinate.toIndex at h₁ ⊢ unfold Array.set simp[←Array.foldl_toList] at h₁ ⊢ - rw[Array.getElem_eq_getElem_toList] at h₁ ⊢ + rw[←Array.getElem_toList] at h₁ ⊢ apply countExitDirections_increasesWhenSet_Aux assumption @@ -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 diff --git a/lakefile.lean b/lakefile.lean index cfea57a..a155aab 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,7 +32,7 @@ lean_exe «aoc-2023» where supportInterpreter := true require BinaryHeap from git - "https://github.com/soulsource/BinaryHeap"@"a2fcff2dbe3561e3a51b810b3f0577ba99ef5e78" + "https://github.com/soulsource/BinaryHeap"@"7896480adb78fc9f9b7a86a5eddd0fc5e3f9e4d5" require «lean-astar» from git - "https://github.com/soulsource/lean-astar"@"6cab1cf9fd9de67f53f9a20a56dc91da38e3544b" + "https://github.com/soulsource/lean-astar"@"dee1a274a1c625462de03b58eaeff82e5db8b830" diff --git a/lean-toolchain b/lean-toolchain index b1c65af..db29c97 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.16.0 +leanprover/lean4:4.17.0 |