From 8054fe2b47861c881ff3b544d68beaf12e983e0f Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Fri, 17 Jan 2025 17:16:44 +0100
Subject: [PATCH] [Kernel] Fix an error in based on map required properties

---
 src/libraries/monads/monad.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/libraries/monads/monad.mli b/src/libraries/monads/monad.mli
index e3f89ca85d..849265e1cc 100644
--- a/src/libraries/monads/monad.mli
+++ b/src/libraries/monads/monad.mli
@@ -167,7 +167,7 @@ end
 
     1. ∀x:'a, ∀f:('a -> 'b), [return (f x) ≣ map f (return x)]
 
-    2. ∀m:('a t t t), [map flatten (flatten m) ≣ flatten (flatten m)]
+    2. ∀m:('a t t t), [flatten (map flatten m) ≣ flatten (flatten m)]
 
     3. ∀m:('a t), [flatten (map return m) ≣ flatten (return m) ≣ m]
 
-- 
GitLab