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