From 74dffd1a83cdd2969a31c9892b0517e7c6f50668 Mon Sep 17 00:00:00 2001
From: Liu Yuxi <ubikium@gmail.com>
Date: Sun, 8 Dec 2024 16:35:07 +0000
Subject: [PATCH] fix: MLList.isEmpty's definition inversed (#1075)

---
 Batteries/Data/MLList/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Data/MLList/Basic.lean b/Batteries/Data/MLList/Basic.lean
index 8ab11c3d80..1553f29061 100644
--- a/Batteries/Data/MLList/Basic.lean
+++ b/Batteries/Data/MLList/Basic.lean
@@ -174,7 +174,7 @@ def fixl [Monad m] {α β : Type u} (f : α → m (α × List β)) (s : α) : ML
 
 /-- Compute, inside the monad, whether a `MLList` is empty. -/
 def isEmpty [Monad m] (xs : MLList m α) : m (ULift Bool) :=
-  (ULift.up ∘ Option.isSome) <$> uncons xs
+  (ULift.up ∘ Option.isNone) <$> uncons xs
 
 /-- Convert a `List` to a `MLList`. -/
 def ofList : List α → MLList m α