diff --git a/tests/lean/run/1218.lean b/tests/lean/run/1218.lean new file mode 100644 index 0000000000..67a132460d --- /dev/null +++ b/tests/lean/run/1218.lean @@ -0,0 +1,2 @@ +example (h : false) : "hello" = "goodbye" := +begin try {reflexivity}, contradiction end