From 296a4ab940c1b70d07a2c560b62e2e4147dbf109 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Nov 2015 12:12:15 -0800 Subject: [PATCH] test(tests/lean/run): add coercion test issue --- tests/lean/run/coe_issue.lean | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 tests/lean/run/coe_issue.lean diff --git a/tests/lean/run/coe_issue.lean b/tests/lean/run/coe_issue.lean new file mode 100644 index 000000000..83b856258 --- /dev/null +++ b/tests/lean/run/coe_issue.lean @@ -0,0 +1,3 @@ +import data.int +open int algebra +example : has_mul int := _