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

---
 Day10.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Day10.lean')

diff --git a/Day10.lean b/Day10.lean
index b7b60ba..fe61825 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -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
-- 
cgit v1.2.3