From 38c00b33113f042d601b100d1c5c288c0ff9f255 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 8 Apr 2025 21:54:27 -0400
Subject: [PATCH] lawfulRunMEvil

---
 SimpleCounterexamples/RunMEvil.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/SimpleCounterexamples/RunMEvil.lean b/SimpleCounterexamples/RunMEvil.lean
index 0be2709..6890720 100644
--- a/SimpleCounterexamples/RunMEvil.lean
+++ b/SimpleCounterexamples/RunMEvil.lean
@@ -6,3 +6,18 @@ instance : Monad EmptyM where
 
 theorem runMEvil (runM : ∀α m, [Monad m] → m α → α) : False :=
   runM PEmpty EmptyM ⟨⟩ |>.elim
+
+instance : LawfulMonad EmptyM where
+  map_const := by intros; trivial
+  id_map := by intros; trivial
+  seqLeft_eq := by intros; trivial
+  seqRight_eq := by intros; trivial
+  pure_seq := by intros; trivial
+  bind_pure_comp := by intros; trivial
+  bind_map := by intros; trivial
+  pure_bind := by intros; trivial
+  bind_assoc := by intros; trivial
+
+theorem lawfulRunMEvil (runM : ∀α m, [Monad m] → [LawfulMonad m] → m α → α)
+    : False :=
+  runM PEmpty EmptyM ⟨⟩ |>.elim