From 0818b02eb3be474429f7c9cd472495d5ba0caa1e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Dec 2016 14:10:47 -0800 Subject: [PATCH] test(tests/lean/run): add test for @1218 --- tests/lean/run/1218.lean | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 tests/lean/run/1218.lean 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