feat(frontends/lean/decl_cmds): closes #791

src/frontends/lean/decl_cmds.cpp

@@ -114,6 +114,12 @@ static void check_parameter_type(parser & p, name const & n, expr const & type,
         });
 }
 
+static environment ensure_decl_namespaces(environment const & env, name const & full_n) {
+    if (full_n.is_atomic())
+        return env;
+    return add_namespace(env, full_n.get_prefix());
+}
+
 static environment declare_var(parser & p, environment env,
                                name const & n, level_param_names const & ls, expr const & type,
                                variable_kind k, optional<binder_info> const & _bi, pos_info const & pos,
@@ -155,6 +161,7 @@ static environment declare_var(parser & p, environment env,
         }
         if (is_protected)
             env = add_protected(env, full_n);
+        env = ensure_decl_namespaces(env, full_n);
         return env;
     }
 }
@@ -885,8 +892,10 @@ class definition_cmd_fn {
                 }
             }
             // TODO(Leo): register aux_decls
-            if (!m_is_private)
+            if (!m_is_private) {
                 m_p.add_decl_index(real_n, m_pos, m_p.get_cmd_token(), type);
+                m_env = ensure_decl_namespaces(m_env, real_n);
+            }
             if (m_is_protected)
                 m_env = add_protected(m_env, real_n);
             if (n != real_n) {

src/library/scoped_ext.cpp

@@ -127,7 +127,11 @@ environment add_namespace(environment const & env, name const & ns) {
     if (!ext.m_namespace_set.contains(ns)) {
         ext.m_namespace_set.insert(ns);
         environment r = update(env, ext);
-        return module::add(r, *g_new_namespace_key, [=](environment const &, serializer & s) { s << ns; });
+        r = module::add(r, *g_new_namespace_key, [=](environment const &, serializer & s) { s << ns; });
+        if (ns.is_atomic())
+            return r;
+        else
+            return add_namespace(r, ns.get_prefix());
     } else {
         return env;
     }

tests/lean/run/791.lean

@@ -0,0 +1,15 @@
+definition foo.bar := 10
+definition boo.bla.foo := 20
+
+open foo
+open boo.bla
+
+eval bar
+eval foo
+
+constant x.y.z : nat
+
+open x
+check y.z
+open x.y
+check z