commit 2573d6489734cbddd411c472c3de11f683a90984 Author: mehbark Date: Tue Apr 8 21:49:57 2025 -0400 runMEvil diff --git a/README.md b/README.md new file mode 100644 index 0000000..741f160 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# simple-counterexamples \ No newline at end of file diff --git a/SimpleCounterexamples.lean b/SimpleCounterexamples.lean new file mode 100644 index 0000000..e69de29 diff --git a/SimpleCounterexamples/RunMEvil.lean b/SimpleCounterexamples/RunMEvil.lean new file mode 100644 index 0000000..0be2709 --- /dev/null +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..b5841a3 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "«simple-counterexamples»", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..44119ce --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,6 @@ +name = "simple-counterexamples" +version = "0.1.0" +defaultTargets = ["SimpleCounterexamples"] + +[[lean_lib]] +name = "SimpleCounterexamples" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..a3edb8f --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.16.0-rc2