fix: MLList.isEmpty's definition inversed (#1075)

leanprover-community · Dec 8, 2024 · 74dffd1 · 74dffd1
1 parent c016aa9
commit 74dffd1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 α