From 626cd952e7a3a11a61d857c99badb91a6eff8419 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Aug 2014 15:23:33 -0700 Subject: [PATCH] test(tests/lean/run): add overload test Signed-off-by: Leonardo de Moura --- tests/lean/run/over2.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 tests/lean/run/over2.lean diff --git a/tests/lean/run/over2.lean b/tests/lean/run/over2.lean new file mode 100644 index 000000000..525648cbe --- /dev/null +++ b/tests/lean/run/over2.lean @@ -0,0 +1,14 @@ +import data.nat +using nat + +namespace N1 + definition foo (a : nat) := a +end N1 + +namespace N2 + definition foo (a : nat) := a +end N2 + +using N1 N2 + +definition boo := foo \ No newline at end of file