feat(frontends/lean): add declaration to namespace without opening it, closes #161

src/frontends/lean/decl_cmds.cpp

@@ -33,7 +33,6 @@ static name g_coercion("[coercion]");
 
 environment universe_cmd(parser & p) {
     name n = p.check_id_next("invalid universe declaration, identifier expected");
-    check_atomic(n);
     environment env = p.env();
     if (in_section_or_context(env)) {
         p.add_local_level(n, mk_param_univ(n));
@@ -119,7 +118,6 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
     auto pos = p.pos();
     optional<binder_info> bi = parse_binder_info(p);
     name n = p.check_id_next("invalid declaration, identifier expected");
-    check_atomic(n);
     buffer<name> ls_buffer;
     if (p.curr_is_token(g_llevel_curly) && in_section_or_context(p.env()))
         throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
@@ -211,7 +209,6 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     auto n_pos = p.pos();
     unsigned start_line = n_pos.first;
     name n     = p.check_id_next("invalid declaration, identifier expected");
-    check_atomic(n);
     decl_modifiers modifiers;
     name real_n; // real name for this declaration
     modifiers.m_is_opaque = _is_opaque;
@@ -382,7 +379,6 @@ static environment variables_cmd(parser & p) {
         buffer<name> ids;
         while (!p.curr_is_token(g_colon)) {
             name id = p.check_id_next("invalid parameters declaration, identifier expected");
-            check_atomic(id);
             ids.push_back(id);
         }
         p.next();

src/frontends/lean/inductive_cmd.cpp

@@ -121,9 +121,9 @@ struct inductive_cmd_fn {
     name parse_decl_name(optional<name> const & ind_name) {
         m_pos   = m_p.pos();
         name id = m_p.check_id_next("invalid declaration, identifier expected");
-        check_atomic(id);
         if (ind_name) {
             // for intro rules, we append the name of the inductive datatype
+            check_atomic(id);
             name full_id = *ind_name + id;
             m_decl_info.emplace_back(full_id, g_intro, m_pos);
             return full_id;

tests/lean/run/ns2.lean

@@ -0,0 +1,29 @@
+definition foo.id {A : Type} (a : A) := a
+variable foo.T : Type.{1}
+check foo.id
+check foo.T
+
+inductive foo.v.I := unit : foo.v.I
+
+check foo.v.I
+check foo.v.I.unit
+
+namespace foo
+  check id
+  check T
+  check v.I
+end foo
+
+namespace bla
+  definition vvv.pr {A : Type} (a b : A) := a
+  check vvv.pr
+end bla
+check bla.vvv.pr
+
+namespace bla
+namespace vvv
+  check pr
+  inductive my.empty : Type
+end vvv
+end bla
+check bla.vvv.my.empty

tests/lean/t3.lean.expected.out

@@ -10,7 +10,6 @@ Type
 Type
 Type
 t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected
-t3.lean:27:0: error: invalid declaration name 'full.name.U', identifier must be atomic
 Type
 Type
 t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level