runMEvil

README.md

@@ -0,0 +1 @@
+# simple-counterexamples

SimpleCounterexamples/RunMEvil.lean

@@ -0,0 +1,8 @@
+structure EmptyM (_ : Type u) : Type v
+
+instance : Monad EmptyM where
+  pure _ := ⟨⟩
+  bind _ _ := ⟨⟩
+
+theorem runMEvil (runM : ∀α m, [Monad m] → m α → α) : False :=
+  runM PEmpty EmptyM ⟨⟩ |>.elim

lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "«simple-counterexamples»",
+ "lakeDir": ".lake"}

lakefile.toml

@@ -0,0 +1,6 @@
+name = "simple-counterexamples"
+version = "0.1.0"
+defaultTargets = ["SimpleCounterexamples"]
+
+[[lean_lib]]
+name = "SimpleCounterexamples"

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.16.0-rc2