diff --git a/src/frontends/lean/cmd_table.h b/src/frontends/lean/cmd_table.h
index 8c7880517a..ec497968fe 100644
--- a/src/frontends/lean/cmd_table.h
+++ b/src/frontends/lean/cmd_table.h
@@ -8,11 +8,19 @@ Author: Leonardo de Moura
 #include <string>
 #include <functional>
 #include "kernel/environment.h"
+#include "frontends/lean/decl_util.h"
 #include "frontends/lean/parser_pos_provider.h"
 
 namespace lean {
 class parser;
-typedef std::function<environment(parser&)> command_fn;
+
+struct cmd_meta {
+    decl_attributes       m_attrs;
+    decl_modifiers        m_modifiers;
+    optional<std::string> m_doc_string;
+};
+
+typedef std::function<environment(parser&, cmd_meta const &)> command_fn;
 
 template<typename F>
 struct cmd_info_tmpl {
@@ -23,6 +31,16 @@ struct cmd_info_tmpl {
 public:
     cmd_info_tmpl(name const & n, char const * d, F const & fn, bool skip_token = true):
         m_name(n), m_descr(d), m_fn(fn), m_skip_token(skip_token) {}
+    cmd_info_tmpl(name const & n, char const * d, std::function<environment(parser&)> const & fn, bool skip_token = true):
+        cmd_info_tmpl(n, d, [=](parser & p, cmd_meta const & meta) {
+            if (meta.m_modifiers)
+                throw exception("command does not accept modifiers");
+            if (meta.m_attrs)
+                throw exception("command does not accept attributes");
+            if (meta.m_doc_string)
+                throw exception("command does not accept doc string");
+            return fn(p);
+        }, skip_token) {}
     cmd_info_tmpl() {}
     name const & get_name() const { return m_name; }
     std::string const & get_descr() const { return m_descr; }
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index 1b920d191f..d8de11cebe 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -36,6 +36,7 @@ public:
     list<entry> const & get_entries() const { return m_entries; }
     bool is_parsing_only() const { return m_parsing_only; }
     optional<unsigned > get_priority() const { return m_prio; }
+    void set_persistent(bool persistent) { m_persistent = persistent; }
     bool ok_for_inductive_type() const;
     bool has_class() const;
     operator bool() const { return static_cast<bool>(m_entries); }
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index c54033e533..34d5e2cfc4 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -92,7 +92,7 @@ static void check_parameter_type(parser & p, name const & n, expr const & type,
 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,
-                               decl_modifiers const & modifiers) {
+                               cmd_meta const & meta) {
     binder_info bi;
     if (_bi) bi = *_bi;
     if (k == variable_kind::Parameter || k == variable_kind::Variable) {
@@ -125,18 +125,18 @@ static environment declare_var(parser & p, environment env,
         if (k == variable_kind::Axiom) {
             env = module::add(env, check(env, mk_axiom(full_n, ls, new_type)));
         } else {
-            bool is_trusted = !modifiers.m_is_meta;
+            bool is_trusted = !meta.m_modifiers.m_is_meta;
             env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type, is_trusted)));
         }
-        if (auto doc = p.get_doc_string())
-            env = add_doc_string(env, full_n, *doc);
+        if (meta.m_doc_string)
+            env = add_doc_string(env, full_n, *meta.m_doc_string);
         if (!ns.is_anonymous()) {
-            if (modifiers.m_is_protected)
+            if (meta.m_modifiers.m_is_protected)
                 env = add_expr_alias(env, get_protected_shortest_name(full_n), full_n);
             else
                 env = add_expr_alias(env, n, full_n);
         }
-        if (modifiers.m_is_protected)
+        if (meta.m_modifiers.m_is_protected)
             env = add_protected(env, full_n);
         env = ensure_decl_namespaces(env, full_n);
         return env;
@@ -190,7 +190,7 @@ static bool curr_is_binder_annotation(parser & p) {
            p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk());
 }
 
-static environment variable_cmd_core(parser & p, variable_kind k, decl_modifiers const & modifiers = decl_modifiers()) {
+static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
     check_variable_kind(p, k);
     auto pos = p.pos();
     module::scope_pos_info scope_pos(pos);
@@ -284,22 +284,24 @@ static environment variable_cmd_core(parser & p, variable_kind k, decl_modifiers
     std::tie(type, new_ls) = p.elaborate_type("_variable", ctx, type);
     if (k == variable_kind::Variable || k == variable_kind::Parameter)
         update_local_levels(p, new_ls, k == variable_kind::Variable);
-    return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, modifiers);
+    return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, meta);
 }
-static environment variable_cmd(parser & p) {
-    return variable_cmd_core(p, variable_kind::Variable);
+static environment variable_cmd(parser & p, cmd_meta const & meta) {
+    return variable_cmd_core(p, variable_kind::Variable, meta);
 }
-static environment axiom_cmd(parser & p)    {
-    return variable_cmd_core(p, variable_kind::Axiom);
+static environment axiom_cmd(parser & p, cmd_meta const & meta)    {
+    if (meta.m_modifiers.m_is_meta)
+        throw exception("invalid 'meta' modifier for axiom");
+    return variable_cmd_core(p, variable_kind::Axiom, meta);
 }
-static environment constant_cmd(parser & p)    {
-    return variable_cmd_core(p, variable_kind::Constant);
+static environment constant_cmd(parser & p, cmd_meta const & meta)    {
+    return variable_cmd_core(p, variable_kind::Constant, meta);
 }
-static environment parameter_cmd(parser & p)    {
-    return variable_cmd_core(p, variable_kind::Parameter);
+static environment parameter_cmd(parser & p, cmd_meta const & meta)    {
+    return variable_cmd_core(p, variable_kind::Parameter, meta);
 }
 
-static environment variables_cmd_core(parser & p, variable_kind k, decl_modifiers const & modifiers = decl_modifiers()) {
+static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
     check_variable_kind(p, k);
     auto pos = p.pos();
     module::scope_pos_info scope_pos(pos);
@@ -325,7 +327,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
                 p.parse_close_binder_info(bi);
                 update_local_binder_info(p, k, id, bi, pos);
                 if (curr_is_binder_annotation(p))
-                    return variables_cmd_core(p, k);
+                    return variables_cmd_core(p, k, meta);
                 else
                     return env;
             } else {
@@ -363,7 +365,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
                     update_local_binder_info(p, k, id, bi, pos);
                 }
                 if (curr_is_binder_annotation(p))
-                    return variables_cmd_core(p, k);
+                    return variables_cmd_core(p, k, meta);
                 else
                     return env;
             } else {
@@ -388,7 +390,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
         if (k == variable_kind::Variable || k == variable_kind::Parameter)
             update_local_levels(p, new_ls, k == variable_kind::Variable);
         new_ls = append(ls, new_ls);
-        env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, modifiers);
+        env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, meta);
     }
     if (curr_is_binder_annotation(p)) {
         if (k == variable_kind::Constant || k == variable_kind::Axiom) {
@@ -396,125 +398,87 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
             // We must do that to be able to process
             //    constants (A : Type) (a : A)
             parser::local_scope scope2(p, env);
-            return variables_cmd_core(p, k);
+            return variables_cmd_core(p, k, meta);
         } else {
-            return variables_cmd_core(p, k);
+            return variables_cmd_core(p, k, meta);
         }
     }
     return env;
 }
-static environment variables_cmd(parser & p) {
-    return variables_cmd_core(p, variable_kind::Variable);
+static environment variables_cmd(parser & p, cmd_meta const & meta) {
+    return variables_cmd_core(p, variable_kind::Variable, meta);
 }
-static environment parameters_cmd(parser & p) {
-    return variables_cmd_core(p, variable_kind::Parameter);
+static environment parameters_cmd(parser & p, cmd_meta const & meta) {
+    return variables_cmd_core(p, variable_kind::Parameter, meta);
 }
-static environment constants_cmd(parser & p) {
-    return variables_cmd_core(p, variable_kind::Constant);
+static environment constants_cmd(parser & p, cmd_meta const & meta) {
+    return variables_cmd_core(p, variable_kind::Constant, meta);
 }
-static environment axioms_cmd(parser & p) {
-    return variables_cmd_core(p, variable_kind::Axiom);
+static environment axioms_cmd(parser & p, cmd_meta const & meta) {
+    return variables_cmd_core(p, variable_kind::Axiom, meta);
 }
 
-static environment definition_cmd_ex(parser & p, decl_attributes const & attributes) {
-    decl_modifiers modifiers;
+static environment definition_cmd(parser & p, cmd_meta const & meta) {
+    return definition_cmd_core(p, def_cmd_kind::Definition, meta);
+}
+static environment theorem_cmd(parser & p, cmd_meta const & meta) {
+    return definition_cmd_core(p, def_cmd_kind::Theorem, meta);
+}
+static environment example_cmd(parser & p, cmd_meta const & meta) {
+    return definition_cmd_core(p, def_cmd_kind::Example, meta);
+}
+static environment instance_cmd(parser & p, cmd_meta const & _meta) {
+    auto meta = _meta;
+    if (meta.m_modifiers.m_is_private)
+        throw exception("invalid 'private' modifier for instance command");
+    if (meta.m_modifiers.m_is_protected)
+        throw exception("invalid 'protected' modifier for instance command");
+    if (meta.m_modifiers.m_is_mutual)
+        throw exception("invalid 'mutual' modifier for instance command");
+    meta.m_modifiers.m_is_protected = true;
+    return definition_cmd_core(p, def_cmd_kind::Instance, meta);
+}
+
+static environment modifiers_cmd(parser & p, cmd_meta const & _meta) {
+    auto meta = _meta;
     if (p.curr_is_token(get_private_tk())) {
-        modifiers.m_is_private = true;
+        meta.m_modifiers.m_is_private = true;
         p.next();
-
-        if (!attributes && p.curr_is_token(get_structure_tk())) {
-            return structure_cmd_ex(p, attributes, modifiers);
-        }
-        if (!attributes && p.curr_is_token(get_class_tk())) {
-            return class_cmd_ex(p, attributes, modifiers);
-        }
     } else if (p.curr_is_token(get_protected_tk())) {
-        modifiers.m_is_protected = true;
+        meta.m_modifiers.m_is_protected = true;
         p.next();
-        if (!attributes) {
-            if (p.curr_is_token_or_id(get_axiom_tk())) {
-                p.next();
-                return variable_cmd_core(p, variable_kind::Axiom, modifiers);
-            } else if (p.curr_is_token_or_id(get_constant_tk())) {
-                p.next();
-                return variable_cmd_core(p, variable_kind::Constant, modifiers);
-            } else if (p.curr_is_token_or_id(get_axioms_tk())) {
-                p.next();
-                return variables_cmd_core(p, variable_kind::Axiom, modifiers);
-            } else if (p.curr_is_token_or_id(get_constants_tk())) {
-                p.next();
-                return variables_cmd_core(p, variable_kind::Constant, modifiers);
-            }
-        }
     }
 
     if (p.curr_is_token(get_noncomputable_tk())) {
-        modifiers.m_is_noncomputable = true;
         p.next();
-
-        if (!attributes && !modifiers.m_is_private && !modifiers.m_is_protected && p.curr_is_token_or_id(get_theory_tk())) {
+        if (!meta.m_attrs && !meta.m_modifiers && p.curr_is_token_or_id(get_theory_tk())) {
+            // `noncomputable theory`
             p.next();
             p.set_ignore_noncomputable();
             return p.env();
+        } else {
+            meta.m_modifiers.m_is_noncomputable = true;
         }
     }
     if (p.curr_is_token(get_meta_tk())) {
-        modifiers.m_is_meta = true;
+        meta.m_modifiers.m_is_meta = true;
         p.next();
-        if (!attributes) {
-            if (p.curr_is_token_or_id(get_constant_tk())) {
-                p.next();
-                return variable_cmd_core(p, variable_kind::Constant, modifiers);
-            } else if (p.curr_is_token_or_id(get_constants_tk())) {
-                p.next();
-                return variables_cmd_core(p, variable_kind::Constant, modifiers);
-            }
-        }
-        if (!modifiers.m_is_private && !modifiers.m_is_protected && p.curr_is_token(get_inductive_tk())) {
-            return inductive_cmd_ex(p, attributes, modifiers.m_is_meta);
-        }
-        if (!attributes && !modifiers.m_is_protected && p.curr_is_token(get_structure_tk())) {
-            return structure_cmd_ex(p, attributes, modifiers);
-        }
-        if (!attributes && !modifiers.m_is_protected && p.curr_is_token(get_class_tk())) {
-            return class_cmd_ex(p, attributes, modifiers);
-        }
     }
 
     if (p.curr_is_token(get_mutual_tk())) {
-        modifiers.m_is_mutual = true;
+        meta.m_modifiers.m_is_mutual = true;
         p.next();
-        if (!modifiers.m_is_private && !modifiers.m_is_protected && !modifiers.m_is_noncomputable &&
-            p.curr_is_token(get_inductive_tk())) {
-            return mutual_inductive_cmd_ex(p, attributes, modifiers.m_is_meta);
-        } else if (!modifiers.m_is_private && !modifiers.m_is_protected && !modifiers.m_is_noncomputable &&
-                   !modifiers.m_is_meta && p.curr_is_token(get_coinductive_tk())) {
-            return mutual_coinductive_cmd_ex(p, attributes);
-        }
     }
 
-    def_cmd_kind kind = Definition;
-    if (p.curr_is_token_or_id(get_definition_tk())) {
-        p.next();
-    } else if (p.curr_is_token_or_id(get_theorem_tk())) {
-        p.next();
-        kind = Theorem;
-    } else if (p.curr_is_token_or_id(get_example_tk())) {
-        p.next();
-        kind = Example;
-    } else if (!modifiers.m_is_private && !modifiers.m_is_protected && p.curr_is_token_or_id(get_instance_tk())) {
-        p.next();
-        modifiers.m_is_protected = true;
-        modifiers.m_is_instance  = true;
-    } else {
-        throw parser_error("invalid definition/theorem, 'definition' or 'theorem' expected", p.pos());
+    if (p.curr_is_token(get_private_tk()) || p.curr_is_token(get_protected_tk()) || p.curr_is_token(get_noncomputable_tk())
+        || p.curr_is_token(get_meta_tk()) || p.curr_is_token(get_mutual_tk())) {
+        throw parser_error("unexpected definition modifier", p.pos());
     }
-
-    return definition_cmd_core(p, kind, modifiers, attributes);
-}
-
-static environment definition_cmd(parser & p) {
-    return definition_cmd_ex(p, {});
+    if (p.curr_is_token(get_attribute_tk()) || p.curr_is_token("@[")) {
+        throw parser_error("unexpected attributes declaration", p.pos());
+    }
+    p.parse_command(meta);
+    return p.env();
 }
 
 static environment attribute_cmd_core(parser & p, bool persistent) {
@@ -523,17 +487,7 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
     attributes.parse(p);
     // 'attribute [attr] definition ...'
     if (p.curr_is_command()) {
-        if (p.curr_is_token_or_id(get_inductive_tk())) {
-            return inductive_cmd_ex(p, attributes, false);
-        } else  if (p.curr_is_token_or_id(get_coinductive_tk())) {
-            return coinductive_cmd_ex(p, attributes);
-        } else  if (p.curr_is_token_or_id(get_structure_tk())) {
-            return structure_cmd_ex(p, attributes, {});
-        } else  if (p.curr_is_token_or_id(get_class_tk())) {
-            return class_cmd_ex(p, attributes, {});
-        } else {
-            return definition_cmd_ex(p, attributes);
-        }
+        return modifiers_cmd(p, {attributes, {}, {}});
     }
     name d          = p.check_constant_next("invalid 'attribute' command, constant expected");
     ds.push_back(d);
@@ -556,21 +510,11 @@ environment local_attribute_cmd(parser & p) {
     return attribute_cmd_core(p, false);
 }
 
-static environment compact_attribute_cmd(parser & p) {
+static environment compact_attribute_cmd(parser & p, cmd_meta const & meta) {
     bool persistent = true;
     decl_attributes attributes(persistent);
     attributes.parse_compact(p);
-    if (p.curr_is_token_or_id(get_inductive_tk())) {
-        return inductive_cmd_ex(p, attributes, false);
-    } else  if (p.curr_is_token_or_id(get_coinductive_tk())) {
-        return coinductive_cmd_ex(p, attributes);
-    } else  if (p.curr_is_token_or_id(get_structure_tk())) {
-        return structure_cmd_ex(p, attributes, {});
-    } else  if (p.curr_is_token_or_id(get_class_tk())) {
-        return class_cmd_ex(p, attributes, {});
-    } else {
-        return definition_cmd_ex(p, attributes);
-    }
+    return modifiers_cmd(p, {attributes, meta.m_modifiers, meta.m_doc_string});
 }
 
 static environment include_cmd_core(parser & p, bool include) {
@@ -614,15 +558,15 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("parameters",      "declare new parameters", parameters_cmd));
     add_cmd(r, cmd_info("constants",       "declare new constants (aka top-level variables)", constants_cmd));
     add_cmd(r, cmd_info("axioms",          "declare new axioms", axioms_cmd));
-    add_cmd(r, cmd_info("definition",      "add new definition", definition_cmd, false));
-    add_cmd(r, cmd_info("meta",            "add new meta definition/constant", definition_cmd, false));
-    add_cmd(r, cmd_info("mutual",          "add new mutal definition/constant/inductive/coinductive", definition_cmd, false));
-    add_cmd(r, cmd_info("noncomputable",   "add new noncomputable definition", definition_cmd, false));
-    add_cmd(r, cmd_info("private",         "add new private definition/theorem", definition_cmd, false));
-    add_cmd(r, cmd_info("protected",       "add new protected definition/theorem/variable", definition_cmd, false));
-    add_cmd(r, cmd_info("theorem",         "add new theorem", definition_cmd, false));
-    add_cmd(r, cmd_info("instance",        "add new instance", definition_cmd, false));
-    add_cmd(r, cmd_info("example",         "add new example", definition_cmd, false));
+    add_cmd(r, cmd_info("meta",            "add new meta declaration", modifiers_cmd, false));
+    add_cmd(r, cmd_info("mutual",          "add new mutal declaration", modifiers_cmd, false));
+    add_cmd(r, cmd_info("noncomputable",   "add new noncomputable definition", modifiers_cmd, false));
+    add_cmd(r, cmd_info("private",         "add new private declaration", modifiers_cmd, false));
+    add_cmd(r, cmd_info("protected",       "add new protected declaration", modifiers_cmd, false));
+    add_cmd(r, cmd_info("definition",      "add new definition", definition_cmd));
+    add_cmd(r, cmd_info("theorem",         "add new theorem", theorem_cmd));
+    add_cmd(r, cmd_info("instance",        "add new instance", instance_cmd));
+    add_cmd(r, cmd_info("example",         "add new example", example_cmd));
     add_cmd(r, cmd_info("include",         "force section parameter/variable to be included", include_cmd));
     add_cmd(r, cmd_info("attribute",       "set declaration attributes", attribute_cmd));
     add_cmd(r, cmd_info("@[",              "declaration attributes", compact_attribute_cmd));
diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h
index 91b9021a56..d67ffd1b21 100644
--- a/src/frontends/lean/decl_util.h
+++ b/src/frontends/lean/decl_util.h
@@ -13,7 +13,7 @@ namespace lean {
 class parser;
 class elaborator;
 
-enum def_cmd_kind { Theorem, Definition, Example };
+enum def_cmd_kind { Theorem, Definition, Example, Instance };
 
 struct decl_modifiers {
     bool m_is_private{false};
@@ -21,8 +21,10 @@ struct decl_modifiers {
     bool m_is_meta{false};
     bool m_is_mutual{false};
     bool m_is_noncomputable{false};
-    bool m_is_instance{false};
-    bool m_is_class{false};
+
+    operator bool() const {
+        return m_is_private || m_is_protected || m_is_meta || m_is_mutual || m_is_noncomputable;
+    }
 };
 
 /** \brief In Lean, declarations may contain nested definitions.
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 3e71c61bd4..e1df34d0ff 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -242,24 +242,23 @@ static environment compile_decl(parser & p, environment const & env,
 
 static pair<environment, name>
 declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffer<name> const & lp_names,
-                   name const & c_name, expr type, optional<expr> val, task<expr> const & proof,
-                   decl_modifiers const & modifiers, decl_attributes attrs, optional<std::string> const & doc_string,
+                   name const & c_name, expr type, optional<expr> val, task<expr> const & proof, cmd_meta const & meta,
                    pos_info const & pos) {
-    auto env_n = mk_real_name(env, c_name, modifiers.m_is_private, pos);
+    auto env_n = mk_real_name(env, c_name, meta.m_modifiers.m_is_private, pos);
     environment new_env = env_n.first;
     name c_real_name    = env_n.second;
-    if (val && modifiers.m_is_meta) {
+    if (val && meta.m_modifiers.m_is_meta) {
         /* TODO(Leo): fix fix_rec_fn_name for mutual definitions.
            We currently do not support meta mutual definitions. Thus, this is not currently an issue. */
         *val = fix_rec_fn_name(*val, c_name, c_real_name);
     }
-    if (val && !modifiers.m_is_meta && !type_checker(env).is_prop(type)) {
+    if (val && !meta.m_modifiers.m_is_meta && !type_checker(env).is_prop(type)) {
         /* We only abstract nested proofs if the type of the definition is not a proposition */
         std::tie(new_env, type) = abstract_nested_proofs(new_env, c_real_name, type);
         std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val);
     }
     bool use_conv_opt = true;
-    bool is_trusted   = !modifiers.m_is_meta;
+    bool is_trusted   = !meta.m_modifiers.m_is_meta;
     auto def          =
         !val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == Theorem ?
         mk_theorem(c_real_name, to_list(lp_names), type, *val) :
@@ -267,23 +266,23 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
     auto cdef         = check(p, new_env, c_name, def, pos);
     new_env           = module::add(new_env, cdef);
 
-    check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, modifiers.m_is_noncomputable, p.get_file_name(), pos);
+    check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, meta.m_modifiers.m_is_noncomputable, p.get_file_name(), pos);
 
-    if (modifiers.m_is_protected)
+    if (meta.m_modifiers.m_is_protected)
         new_env = add_protected(new_env, c_real_name);
 
-    new_env = add_alias(new_env, modifiers.m_is_protected, c_name, c_real_name);
+    new_env = add_alias(new_env, meta.m_modifiers.m_is_protected, c_name, c_real_name);
 
-    if (!modifiers.m_is_private) {
+    if (!meta.m_modifiers.m_is_private) {
         new_env = ensure_decl_namespaces(new_env, c_real_name);
     }
 
     new_env = compile_decl(p, new_env, c_name, c_real_name, pos);
-    if (doc_string) {
-        new_env = add_doc_string(new_env, c_real_name, *doc_string);
+    if (meta.m_doc_string) {
+        new_env = add_doc_string(new_env, c_real_name, *meta.m_doc_string);
     }
     // note: some attribute handlers rely on the new definition being compiled already
-    new_env = attrs.apply(new_env, p.ios(), c_real_name);
+    new_env = meta.m_attrs.apply(new_env, p.ios(), c_real_name);
     return mk_pair(new_env, c_real_name);
 }
 
@@ -470,16 +469,16 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
     return copy_equation_lemmas(env, d_names);
 }
 
-environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modifiers const & modifiers, decl_attributes attrs) {
+static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
     buffer<name> lp_names;
     buffer<expr> fns, params;
-    declaration_info_scope scope(p, kind, modifiers);
+    declaration_info_scope scope(p, kind, meta.m_modifiers);
     auto header_pos = p.pos();
     /* TODO(Leo): allow a different doc string for each function in a mutual definition. */
-    optional<std::string> doc_string = p.get_doc_string();
+    optional<std::string> doc_string = meta.m_doc_string;
     expr val = parse_mutual_definition(p, lp_names, fns, params);
 
-    if (modifiers.m_is_meta) {
+    if (meta.m_modifiers.m_is_meta) {
         throw exception("support for mutual meta definitions has not been implemented yet");
     }
 
@@ -505,13 +504,12 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     for (unsigned i = 0; i < num_defs; i++) {
         expr curr      = get_equations_result(val, i);
         expr curr_type = head_beta_reduce(elab.infer_type(curr));
-        finalize_definition(elab, new_params, curr_type, curr, lp_names, modifiers.m_is_meta);
+        finalize_definition(elab, new_params, curr_type, curr, lp_names, meta.m_modifiers.m_is_meta);
         environment env = elab.env();
         name c_name = mlocal_name(fns[i]);
         name c_real_name;
         std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name,
-                                                        curr_type, some_expr(curr), {}, modifiers, attrs,
-                                                        doc_string, header_pos);
+                                                        curr_type, some_expr(curr), {}, meta, header_pos);
         new_d_names.push_back(c_real_name);
         elab.set_env(env);
     }
@@ -768,21 +766,20 @@ static bool is_rfl_preexpr(expr const & e) {
     return is_constant(e, get_rfl_name());
 }
 
-environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modifiers modifiers, decl_attributes attrs) {
+environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta meta) {
     buffer<name> lp_names;
     buffer<expr> params;
     expr fn, val;
     auto header_pos = p.pos();
-    optional<std::string> doc_string = p.get_doc_string();
     module::scope_pos_info scope_pos(header_pos);
-    declaration_info_scope scope(p, kind, modifiers);
+    declaration_info_scope scope(p, kind, meta.m_modifiers);
     bool is_example  = (kind == def_cmd_kind::Example);
-    bool is_instance = modifiers.m_is_instance;
+    bool is_instance = (kind == def_cmd_kind::Instance);
     bool aux_lemmas  = scope.gen_aux_lemmas();
     bool is_rfl      = false;
     if (is_instance)
-        attrs.set_attribute(p.env(), "instance");
-    std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, modifiers.m_is_meta);
+        meta.m_attrs.set_attribute(p.env(), "instance");
+    std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta);
 
     auto begin_pos = p.cmd_pos();
     auto end_pos = p.pos();
@@ -827,8 +824,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
                                        new_fn, val, thm_finfo, is_rfl, type,
                                        mctx, lctx, pos_provider, use_info_manager, file_name);
             }), log_tree::ElaborationLevel);
-            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, modifiers, attrs,
-                                       doc_string, header_pos);
+            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, meta, header_pos);
         } else if (kind == Example) {
             auto env = p.env();
             auto opts = p.get_options();
@@ -841,7 +837,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
             bool noncomputable_theory = p.ignore_noncomputable();
             std::string file_name = p.get_file_name();
             add_library_task<unit>([=] {
-                check_example(env, opts, modifiers, noncomputable_theory,
+                check_example(env, opts, meta.m_modifiers, noncomputable_theory,
                               lp_name_list, new_params_list, fn, val, mctx, lctx,
                               pos_provider, use_info_manager, file_name);
                 return unit();
@@ -849,7 +845,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
             return p.env();
         } else {
             std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
-            if (modifiers.m_is_meta) {
+            if (meta.m_modifiers.m_is_meta) {
                 val = fix_rec_fn_macro_args(elab, mlocal_name(fn), new_params, type, val);
             }
             eqns = is_equations_result(val);
@@ -858,9 +854,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
                 lean_assert(get_equations_result_size(val) == 1);
                 val = get_equations_result(val, 0);
             }
-            finalize_definition(elab, new_params, type, val, lp_names, modifiers.m_is_meta);
+            finalize_definition(elab, new_params, type, val, lp_names, meta.m_modifiers.m_is_meta);
             env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, some_expr(val),
-                                       {}, modifiers, attrs, doc_string, header_pos);
+                                       {}, meta, header_pos);
         }
         environment new_env = env_n.first;
         name c_real_name    = env_n.second;
@@ -869,9 +865,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
         if (eqns && aux_lemmas) {
             new_env = copy_equation_lemmas(new_env, c_real_name);
         }
-        if (!eqns && !modifiers.m_is_meta && kind == Definition) {
+        if (!eqns && !meta.m_modifiers.m_is_meta && (kind == Definition || kind == Instance)) {
             unsigned arity = new_params.size();
-            new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), modifiers.m_is_private, c_real_name, arity);
+            new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), meta.m_modifiers.m_is_private, c_real_name, arity);
         }
         return new_env;
     };
@@ -890,10 +886,10 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     }
 }
 
-environment definition_cmd_core(parser & p, def_cmd_kind kind, decl_modifiers const & modifiers, decl_attributes attrs) {
-    if (modifiers.m_is_mutual)
-        return mutual_definition_cmd_core(p, kind, modifiers, attrs);
+environment definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
+    if (meta.m_modifiers.m_is_mutual)
+        return mutual_definition_cmd_core(p, kind, meta);
     else
-        return single_definition_cmd_core(p, kind, modifiers, attrs);
+        return single_definition_cmd_core(p, kind, meta);
 }
 }
diff --git a/src/frontends/lean/definition_cmds.h b/src/frontends/lean/definition_cmds.h
index 0fe336e466..90eb58c0e1 100644
--- a/src/frontends/lean/definition_cmds.h
+++ b/src/frontends/lean/definition_cmds.h
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 namespace lean {
 
-environment definition_cmd_core(parser & p, def_cmd_kind k, decl_modifiers const & modifies, decl_attributes attributes);
+environment definition_cmd_core(parser & p, def_cmd_kind k, cmd_meta const & meta);
 
 environment ensure_decl_namespaces(environment const & env, name const & full_n);
 }
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index a6589dd536..963425b77b 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -89,8 +89,7 @@ static level subtract_from_max(level const & l, unsigned offset) {
 class inductive_cmd_fn {
     parser &                        m_p;
     environment                     m_env;
-    decl_attributes                 m_attrs;
-    bool                            m_is_trusted;
+    cmd_meta                        m_meta_info;
     buffer<decl_attributes>         m_mut_attrs;
     type_context                    m_ctx;
     buffer<name>                    m_lp_names;
@@ -102,7 +101,6 @@ class inductive_cmd_fn {
     unsigned                        m_u_param_offset;
 
     bool                            m_infer_result_universe{false};
-    optional<std::string>           m_doc_string;
 
     [[ noreturn ]] void throw_error(char const * error_msg) const { throw parser_error(error_msg, m_pos); }
     [[ noreturn ]] void throw_error(sstream const & strm) const { throw parser_error(strm, m_pos); }
@@ -568,9 +566,6 @@ class inductive_cmd_fn {
         parser::local_scope scope(m_p);
         m_pos = m_p.pos();
 
-        m_attrs.parse(m_p);
-        check_attrs(m_attrs);
-
         declaration_name_scope nscope;
         expr ind = parse_single_header(m_p, nscope, m_lp_names, params);
         m_explicit_levels = !m_lp_names.empty();
@@ -602,9 +597,6 @@ class inductive_cmd_fn {
     void parse_mutual_inductive(buffer<expr> & params, buffer<expr> & inds, buffer<buffer<expr> > & intro_rules) {
         parser::local_scope scope(m_p);
 
-        m_attrs.parse(m_p);
-        check_attrs(m_attrs);
-
         buffer<expr> pre_inds;
         parse_mutual_header(m_p, m_lp_names, pre_inds, params);
         m_explicit_levels = !m_lp_names.empty();
@@ -641,25 +633,33 @@ class inductive_cmd_fn {
         if (!attrs.ok_for_inductive_type())
             throw_error("only attribute [class] accepted for inductive types");
     }
+
+    void check_modifiers() const {
+        if (m_meta_info.m_modifiers.m_is_noncomputable)
+            throw_error("invalid 'noncomputable' modifier for inductive type");
+        if (m_meta_info.m_modifiers.m_is_private)
+            throw_error("invalid 'private' modifier for inductive type");
+        if (m_meta_info.m_modifiers.m_is_protected)
+            throw_error("invalid 'protected' modifier for inductive type");
+    }
 public:
-    inductive_cmd_fn(parser & p, decl_attributes const & attrs, bool is_trusted):
-        m_p(p), m_env(p.env()), m_attrs(attrs),
-        m_is_trusted(is_trusted), m_ctx(p.env()) {
+    inductive_cmd_fn(parser & p, cmd_meta const & meta):
+        m_p(p), m_env(p.env()), m_meta_info(meta), m_ctx(p.env()) {
         m_u_meta = m_ctx.mk_univ_metavar_decl();
-        check_attrs(m_attrs);
-        m_doc_string = p.get_doc_string();
+        check_attrs(m_meta_info.m_attrs);
+        check_modifiers();
     }
 
     void post_process(buffer<expr> const & new_params, buffer<expr> const & new_inds, buffer<buffer<expr> > const & new_intro_rules) {
         add_aliases(new_params, new_inds, new_intro_rules);
         add_namespaces(new_inds);
         for (expr const & ind : new_inds) {
-            m_env = m_attrs.apply(m_env, m_p.ios(), mlocal_name(ind));
+            m_env = m_meta_info.m_attrs.apply(m_env, m_p.ios(), mlocal_name(ind));
             /* TODO(Leo): add support for doc-strings in mutual inductive definitions.
                We are currently using the same doc string for all elements.
             */
-            if (m_doc_string)
-                m_env = add_doc_string(m_env, mlocal_name(ind), *m_doc_string);
+            if (m_meta_info.m_doc_string)
+                m_env = add_doc_string(m_env, mlocal_name(ind), *m_meta_info.m_doc_string);
         }
         if (!m_mut_attrs.empty()) {
             lean_assert(new_inds.size() == m_mut_attrs.size());
@@ -668,7 +668,17 @@ public:
         }
     }
 
-    environment shared_inductive_cmd(buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules) {
+    environment inductive_cmd() {
+        buffer<expr> params;
+        buffer<expr> inds;
+        buffer<buffer<expr> > intro_rules;
+        if (m_meta_info.m_modifiers.m_is_mutual) {
+            parse_mutual_inductive(params, inds, intro_rules);
+        } else {
+            intro_rules.emplace_back();
+            inds.push_back(parse_inductive(params, intro_rules.back()));
+        }
+
         buffer<expr> new_params;
         buffer<expr> new_inds;
         buffer<buffer<expr> > new_intro_rules;
@@ -677,31 +687,21 @@ public:
         }
         elaborate_inductive_decls(params, inds, intro_rules, new_params, new_inds, new_intro_rules);
         m_env = add_inductive_declaration(m_p.env(), m_p.get_options(), m_implicit_infer_map, m_lp_names, new_params,
-                                          new_inds, new_intro_rules, m_is_trusted);
+                                          new_inds, new_intro_rules, !m_meta_info.m_modifiers.m_is_meta);
         post_process(new_params, new_inds, new_intro_rules);
         return m_env;
     }
 
-    environment inductive_cmd() {
+    environment coinductive_cmd() {
         buffer<expr> params;
         buffer<expr> inds;
         buffer<buffer<expr> > intro_rules;
-        intro_rules.emplace_back();
-        inds.push_back(parse_inductive(params, intro_rules.back()));
-        return shared_inductive_cmd(params, inds, intro_rules);
-    }
-
-    environment mutual_inductive_cmd() {
-        buffer<expr> params;
-        buffer<expr> inds;
-        buffer<buffer<expr> > intro_rules;
-        parse_mutual_inductive(params, inds, intro_rules);
-        return shared_inductive_cmd(params, inds, intro_rules);
-    }
-
-    environment shared_coinductive_cmd(buffer<expr> const & params,
-                                       buffer<expr> const & inds,
-                                       buffer<buffer<expr> > const & intro_rules) {
+        if (m_meta_info.m_modifiers.m_is_mutual) {
+            parse_mutual_inductive(params, inds, intro_rules);
+        } else {
+            intro_rules.emplace_back();
+            inds.push_back(parse_inductive(params, intro_rules.back()));
+        }
         buffer<expr> new_params;
         buffer<expr> new_inds;
         buffer<buffer<expr> > new_intro_rules;
@@ -734,59 +734,20 @@ public:
 
         throw generic_exception(first_ind, "coinduction command failed");
     }
-
-    environment coinductive_cmd() {
-        buffer<expr> params;
-        buffer<expr> inds;
-        buffer<buffer<expr> > intro_rules;
-        intro_rules.emplace_back();
-        inds.push_back(parse_inductive(params, intro_rules.back()));
-        return shared_coinductive_cmd(params, inds, intro_rules);
-    }
-
-    environment mutual_coinductive_cmd() {
-        buffer<expr> params;
-        buffer<expr> inds;
-        buffer<buffer<expr> > intro_rules;
-        parse_mutual_inductive(params, inds, intro_rules);
-        return shared_coinductive_cmd(params, inds, intro_rules);
-    }
 };
 
-environment inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta) {
+environment inductive_cmd(parser & p, cmd_meta const & meta) {
     p.next();
     auto pos = p.pos();
     module::scope_pos_info scope_pos(pos);
-    return inductive_cmd_fn(p, attrs, !is_meta).inductive_cmd();
+    return inductive_cmd_fn(p, meta).inductive_cmd();
 }
 
-environment mutual_inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta) {
+environment coinductive_cmd(parser & p, cmd_meta const & meta) {
     p.next();
     auto pos = p.pos();
     module::scope_pos_info scope_pos(pos);
-    return inductive_cmd_fn(p, attrs, !is_meta).mutual_inductive_cmd();
-}
-
-environment coinductive_cmd_ex(parser & p, decl_attributes const & attrs) {
-    p.next();
-    auto pos = p.pos();
-    module::scope_pos_info scope_pos(pos);
-    return inductive_cmd_fn(p, attrs, true).coinductive_cmd();
-}
-
-environment mutual_coinductive_cmd_ex(parser & p, decl_attributes const & attrs) {
-    p.next();
-    auto pos = p.pos();
-    module::scope_pos_info scope_pos(pos);
-    return inductive_cmd_fn(p, attrs, true).mutual_coinductive_cmd();
-}
-
-environment inductive_cmd(parser & p) {
-    return inductive_cmd_ex(p, {}, false);
-}
-
-environment coinductive_cmd(parser & p) {
-    return coinductive_cmd_ex(p, {});
+    return inductive_cmd_fn(p, meta).coinductive_cmd();
 }
 
 void register_inductive_cmds(cmd_table & r) {
diff --git a/src/frontends/lean/inductive_cmds.h b/src/frontends/lean/inductive_cmds.h
index 779d555089..7fa1417338 100644
--- a/src/frontends/lean/inductive_cmds.h
+++ b/src/frontends/lean/inductive_cmds.h
@@ -8,10 +8,8 @@ Author: Daniel Selsam
 #include "frontends/lean/cmd_table.h"
 #include "frontends/lean/decl_attributes.h"
 namespace lean {
-environment inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta);
-environment mutual_inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta);
-environment coinductive_cmd_ex(parser & p, decl_attributes const & attrs);
-environment mutual_coinductive_cmd_ex(parser & p, decl_attributes const & attrs);
+environment inductive_cmd(parser & p, cmd_meta const & meta);
+environment coinductive_cmd(parser & p, cmd_meta const & meta);
 
 void register_inductive_cmds(cmd_table & r);
 void initialize_inductive_cmds();
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 6598027d5e..00fa1a7b06 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2270,22 +2270,15 @@ public:
     virtual optional<expr> is_stuck(expr const & e) override { return ctx().is_stuck(e); }
 };
 
-static name_set * g_documentable_cmds = nullptr;
-
-static bool support_docummentation(name const & n) {
-    return g_documentable_cmds->contains(n);
-}
-
-void parser::parse_command() {
-    lean_assert(curr() == token_kind::CommandKeyword);
+void parser::parse_command(cmd_meta const & meta) {
+    if (curr() != token_kind::CommandKeyword) {
+        auto p = pos();
+        maybe_throw_error({"expected command", p});
+        return;
+    }
     m_last_cmd_pos = pos();
     name cmd_name = get_token_info().value();
     m_cmd_token = get_token_info().token();
-    if (m_doc_string && !support_docummentation(cmd_name)) {
-        next();
-        reset_doc_string();
-        maybe_throw_error({sstream() << "command '" << cmd_name << "' does not support doc string", m_last_cmd_pos});
-    }
     if (auto it = cmds().find(cmd_name)) {
         lazy_type_context tc(m_env, get_options());
         scope_global_ios scope1(m_ios);
@@ -2295,24 +2288,23 @@ void parser::parse_command() {
             in_notation_ctx ctx(*this);
             if (it->get_skip_token())
                 next();
-            m_env = it->get_fn()(*this);
+            m_env = it->get_fn()(*this, meta);
         } else {
             if (it->get_skip_token())
                 next();
-            m_env = it->get_fn()(*this);
+            m_env = it->get_fn()(*this, meta);
         }
     } else {
-        reset_doc_string();
         auto p = pos();
         next();
         maybe_throw_error({sstream() << "unknown command '" << cmd_name << "'", p});
     }
-    reset_doc_string();
 }
 
-void parser::parse_doc_block() {
-    m_doc_string = m_scanner.get_str_val();
+std::string parser::parse_doc_block() {
+    auto val = m_scanner.get_str_val();
     next();
+    return val;
 }
 
 void parser::parse_mod_doc_block() {
@@ -2320,19 +2312,6 @@ void parser::parse_mod_doc_block() {
     next();
 }
 
-void parser::check_no_doc_string() {
-    if (m_doc_string) {
-        auto p = pos();
-        next();
-        reset_doc_string();
-        maybe_throw_error({"invalid occurrence of doc string immediately before current position", p});
-    }
-}
-
-void parser::reset_doc_string() {
-    m_doc_string = optional<std::string>();
-}
-
 #if defined(__GNUC__) && !defined(__CLANG__)
 #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
 #endif
@@ -2494,29 +2473,22 @@ bool parser::parse_command_like() {
 
     switch (curr()) {
         case token_kind::CommandKeyword:
-            if (curr_is_token(get_end_tk())) {
-                check_no_doc_string();
-            }
-            parse_command();
+            parse_command({});
             updt_options();
             break;
         case token_kind::DocBlock:
-            check_no_doc_string();
-            parse_doc_block();
+            parse_command({{}, {}, some(parse_doc_block())});
             break;
         case token_kind::ModDocBlock:
-            check_no_doc_string();
             parse_mod_doc_block();
             break;
         case token_kind::Eof:
-            check_no_doc_string();
             if (has_open_scopes(m_env)) {
                 maybe_throw_error({"invalid end of module, expecting 'end'", pos()});
             }
             return true;
             break;
         case token_kind::Keyword:
-            check_no_doc_string();
             if (curr_is_token(get_period_tk())) {
                 next();
                 break;
@@ -2633,26 +2605,10 @@ void initialize_parser() {
     register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
                          "(lean parser) display error messages in the regular output channel");
     g_tmp_prefix = new name(name::mk_internal_unique_name());
-    g_documentable_cmds = new name_set();
-
-    g_documentable_cmds->insert("definition");
-    g_documentable_cmds->insert("theorem");
-    g_documentable_cmds->insert("constant");
-    g_documentable_cmds->insert("axiom");
-    g_documentable_cmds->insert("meta");
-    g_documentable_cmds->insert("mutual");
-    g_documentable_cmds->insert("@[");
-    g_documentable_cmds->insert("protected");
-    g_documentable_cmds->insert("class");
-    g_documentable_cmds->insert("instance");
-    g_documentable_cmds->insert("inductive");
-    g_documentable_cmds->insert("coinductive");
-    g_documentable_cmds->insert("structure");
 }
 
 void finalize_parser() {
     delete g_tmp_prefix;
     delete g_parser_show_errors;
-    delete g_documentable_cmds;
 }
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 06066078e3..088665989e 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/local_level_decls.h"
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/local_context_adapter.h"
+#include "frontends/lean/decl_util.h"
 
 namespace lean {
 struct interrupt_parser {};
@@ -83,9 +84,6 @@ class parser : public abstract_parser {
     // noncomputable definitions not tagged as noncomputable.
     bool                   m_ignore_noncomputable;
 
-    // Docgen
-    optional<std::string>  m_doc_string;
-
     void sync_command();
 
     tag get_tag(expr e);
@@ -96,13 +94,10 @@ class parser : public abstract_parser {
     level parse_level_nud();
     level parse_level_led(level left);
 
-    void parse_doc_block();
+    std::string parse_doc_block();
     void parse_mod_doc_block();
-    void check_no_doc_string();
-    void reset_doc_string();
 
     void process_imports();
-    void parse_command();
     bool parse_command_like();
     void process_postponed(buffer<expr> const & args, bool is_left, buffer<notation::action_kind> const & kinds,
                            buffer<list<expr>> const & nargs, buffer<expr> const & ps, buffer<pair<unsigned, pos_info>> const & scoped_info,
@@ -242,8 +237,6 @@ public:
     pos_info cmd_pos() const { return m_last_cmd_pos; }
     name const & get_cmd_token() const { return m_cmd_token; }
 
-    optional<std::string> get_doc_string() const { return m_doc_string; }
-
     parser_pos_provider get_parser_pos_provider(pos_info const & some_pos) const {
         return parser_pos_provider(m_pos_table, m_file_name, some_pos, m_next_tag_idx);
     }
@@ -413,6 +406,7 @@ public:
     expr parse_scoped_expr(buffer<expr> const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
     expr parse_expr_with_env(local_environment const & lenv, unsigned rbp = 0);
 
+    void parse_command(cmd_meta const & meta);
     void parse_imports(unsigned & fingerprint, std::vector<module_name> &);
 
     struct local_scope {
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index b8a7e8a96e..7e5d911235 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -256,16 +256,14 @@ struct structure_cmd_fn {
     };
 
     parser &                    m_p;
-    decl_modifiers              m_modifiers;
+    cmd_meta                    m_meta_info;
     environment                 m_env;
     type_context                m_ctx;
     name                        m_namespace;
     name                        m_name;
     name                        m_given_name;
-    optional<std::string>       m_doc_string;
     pos_info                    m_name_pos;
     buffer<name>                m_level_names;
-    decl_attributes             m_attrs;
     buffer<expr>                m_params;
     expr                        m_type;
     buffer<optional<name>>      m_parent_refs;
@@ -286,31 +284,24 @@ struct structure_cmd_fn {
     buffer<expr>                m_ctx_locals; // context local constants for creating aliases
     unsigned                    m_prio;
 
-    structure_cmd_fn(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers):
+    structure_cmd_fn(parser & p, cmd_meta const & meta):
         m_p(p),
-        m_modifiers(modifiers),
+        m_meta_info(meta),
         m_env(p.env()),
         m_ctx(p.env()),
-        m_namespace(get_namespace(m_env)),
-        m_attrs(attrs) {
+        m_namespace(get_namespace(m_env)) {
         m_explicit_universe_params = false;
         m_infer_result_universe    = false;
         m_inductive_predicate      = false;
         m_subobjects               = !p.get_options().get_bool("old_structure_cmd", false);
         m_prio                     = get_default_priority(p.get_options());
-        m_doc_string               = p.get_doc_string();
-    }
-
-    void check_attrs(decl_attributes const & attrs, pos_info const & pos) const {
-        if (!attrs.ok_for_inductive_type())
-            throw parser_error("only attribute [class] accepted for structures", pos);
+        if (!meta.m_attrs.ok_for_inductive_type())
+            throw exception("only attribute [class] accepted for structures");
     }
 
     /** \brief Parse structure name and (optional) universe parameters */
     void parse_decl_name() {
         m_name_pos = m_p.pos();
-        m_attrs.parse(m_p);
-        check_attrs(m_attrs, m_name_pos);
         buffer<name> ls_buffer;
         if (parse_univ_params(m_p, ls_buffer)) {
             m_explicit_universe_params = true;
@@ -319,7 +310,7 @@ struct structure_cmd_fn {
             m_explicit_universe_params = false;
         }
         m_given_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
-        if (m_modifiers.m_is_private) {
+        if (m_meta_info.m_modifiers.m_is_private) {
             unsigned h   = hash(m_name_pos.first, m_name_pos.second);
             auto env_n   = add_private_name(m_env, m_given_name, optional<unsigned>(h));
             m_env        = env_n.first;
@@ -1017,7 +1008,7 @@ struct structure_cmd_fn {
         levels rec_ctx_levels;
         if (!is_nil(m_ctx_levels))
             rec_ctx_levels = levels(mk_level_placeholder(), m_ctx_levels);
-        if (m_modifiers.m_is_private) {
+        if (m_meta_info.m_modifiers.m_is_private) {
             name given_rec_name = name(m_given_name, n.get_string());
             m_env = ::lean::add_alias(m_p, m_env, given_rec_name, n, rec_ctx_levels, m_ctx_locals);
         } else {
@@ -1033,7 +1024,7 @@ struct structure_cmd_fn {
         level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end());
         inductive::intro_rule intro = inductive::mk_intro_rule(m_mk, intro_type);
         inductive::inductive_decl  decl(m_name, lnames, m_params.size(), structure_type, to_list(intro));
-        bool is_trusted = !m_modifiers.m_is_meta;
+        bool is_trusted = !m_meta_info.m_modifiers.m_is_meta;
         m_env = module::add_inductive(m_env, decl, is_trusted);
         name rec_name = inductive::get_elim_name(m_name);
         m_env = add_namespace(m_env, m_name);
@@ -1041,7 +1032,7 @@ struct structure_cmd_fn {
         add_alias(m_given_name, m_name);
         add_alias(m_mk);
         add_rec_alias(rec_name);
-        m_env = m_attrs.apply(m_env, m_p.ios(), m_name);
+        m_env = m_meta_info.m_attrs.apply(m_env, m_p.ios(), m_name);
 
         m_env = add_structure_declaration_aux(m_env, m_p.get_options(), m_level_names, m_params,
                                               mk_local(m_name, mk_structure_type_no_params()),
@@ -1052,7 +1043,7 @@ struct structure_cmd_fn {
         buffer<name> proj_names = get_structure_fields(m_env, m_name);
         for (auto & n : proj_names)
             n = m_name + n;
-        m_env = mk_projections(m_env, m_name, proj_names, m_mk_infer, m_attrs.has_class());
+        m_env = mk_projections(m_env, m_name, proj_names, m_mk_infer, m_meta_info.m_attrs.has_class());
         for (auto const & n : proj_names)
             add_alias(n);
     }
@@ -1101,7 +1092,8 @@ struct structure_cmd_fn {
                 declaration new_decl = mk_definition_inferring_trusted(m_env, decl_name, decl_lvls,
                                                                        decl_type, decl_value, reducibility_hints::mk_abbreviation());
                 m_env = module::add(m_env, check(m_env, new_decl));
-                m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(), m_modifiers.m_is_private, decl_name, args.size());
+                m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(),
+                                                     m_meta_info.m_modifiers.m_is_private, decl_name, args.size());
                 m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true);
             }
         }
@@ -1173,7 +1165,7 @@ struct structure_cmd_fn {
             name const & parent_name       = const_name(parent_fn);
             if (m_subobjects) {
                 if (!m_private_parents[i]) {
-                    if (m_attrs.has_class() && is_class(m_env, parent_name)) {
+                    if (m_meta_info.m_attrs.has_class() && is_class(m_env, parent_name)) {
                         // if both are classes, then we also mark coercion_name as an instance
                         m_env = add_instance(m_env, m_name + m_fields[i].get_name(), m_prio, true);
                     }
@@ -1191,7 +1183,7 @@ struct structure_cmd_fn {
             level parent_rlvl              = sort_level(parent_type);
             expr st_type                   = mk_app(mk_constant(m_name, st_ls), m_params);
             binder_info bi;
-            if (m_attrs.has_class())
+            if (m_meta_info.m_attrs.has_class())
                 bi = mk_inst_implicit_binder_info();
             expr st                        = mk_local(mk_fresh_name(), "s", st_type, bi);
             expr coercion_type             = infer_implicit(Pi(m_params, Pi(st, parent, m_p), m_p), m_params.size(), true);;
@@ -1210,7 +1202,7 @@ struct structure_cmd_fn {
             add_alias(coercion_name);
             m_env = vm_compile(m_env, m_env.get(coercion_name));
             if (!m_private_parents[i]) {
-                if (m_attrs.has_class() && is_class(m_env, parent_name)) {
+                if (m_meta_info.m_attrs.has_class() && is_class(m_env, parent_name)) {
                     // if both are classes, then we also mark coercion_name as an instance
                     m_env = add_instance(m_env, coercion_name, m_prio, true);
                 }
@@ -1241,8 +1233,8 @@ struct structure_cmd_fn {
     }
 
     void add_doc_string() {
-        if (m_doc_string)
-            m_env = ::lean::add_doc_string(m_env, m_name, *m_doc_string);
+        if (m_meta_info.m_doc_string)
+            m_env = ::lean::add_doc_string(m_env, m_name, *m_meta_info.m_doc_string);
     }
 
     environment operator()() {
@@ -1288,29 +1280,23 @@ struct structure_cmd_fn {
     }
 };
 
-environment structure_cmd_ex(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers) {
+environment structure_cmd(parser & p, cmd_meta const & meta) {
     p.next();
-    return structure_cmd_fn(p, attrs, modifiers)();
+    return structure_cmd_fn(p, meta)();
 }
 
-environment structure_cmd(parser & p) {
-    return structure_cmd_ex(p, {}, {});
-}
-
-environment class_cmd_ex(parser & p, decl_attributes attrs, decl_modifiers const & modifiers) {
-    attrs.set_attribute(p.env(), "class");
+environment class_cmd(parser & p, cmd_meta const & _meta) {
+    auto meta = _meta;
+    meta.m_attrs.set_persistent(true);
+    meta.m_attrs.set_attribute(p.env(), "class");
     p.next();
     if (p.curr_is_token(get_inductive_tk())) {
-        return inductive_cmd_ex(p, attrs, modifiers.m_is_meta);
+        return inductive_cmd(p, meta);
     } else {
-        return structure_cmd_fn(p, attrs, modifiers)();
+        return structure_cmd_fn(p, meta)();
     }
 }
 
-environment class_cmd(parser & p) {
-    return class_cmd_ex(p, {}, {});
-}
-
 void register_structure_cmd(cmd_table & r) {
     add_cmd(r, cmd_info("structure",   "declare a new structure/record type", structure_cmd, false));
     add_cmd(r, cmd_info("class",       "declare a new class", class_cmd, false));
diff --git a/src/frontends/lean/structure_cmd.h b/src/frontends/lean/structure_cmd.h
index 12382be8bb..277abc339d 100644
--- a/src/frontends/lean/structure_cmd.h
+++ b/src/frontends/lean/structure_cmd.h
@@ -9,8 +9,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/cmd_table.h"
 namespace lean {
-environment structure_cmd_ex(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers);
-environment class_cmd_ex(parser & p, decl_attributes attrs, decl_modifiers const & modifiers);
+environment structure_cmd(parser & p, cmd_meta const & meta);
+environment class_cmd(parser & p, cmd_meta const & meta);
 buffer<name> get_structure_fields(environment const & env, name const & S);
 void register_structure_cmd(cmd_table & r);
 /** \brief Return true iff \c S is a structure created with the structure command */
diff --git a/tests/lean/bad_unification_hint.lean.expected.out b/tests/lean/bad_unification_hint.lean.expected.out
index 018a219da8..bbd013b1ab 100644
--- a/tests/lean/bad_unification_hint.lean.expected.out
+++ b/tests/lean/bad_unification_hint.lean.expected.out
@@ -1,4 +1,4 @@
-bad_unification_hint.lean:7:0: error: invalid unification hint, failed to unify pattern after unifying constraints
-bad_unification_hint.lean:7:0: warning: declaration 'append_cons_hint' uses sorry
-bad_unification_hint.lean:12:0: error: invalid unification hint, failed to unify constraint #1
-bad_unification_hint.lean:12:0: warning: declaration 'cons_append_hint'' uses sorry
+bad_unification_hint.lean:7:9: error: invalid unification hint, failed to unify pattern after unifying constraints
+bad_unification_hint.lean:7:9: warning: declaration 'append_cons_hint' uses sorry
+bad_unification_hint.lean:12:9: error: invalid unification hint, failed to unify constraint #1
+bad_unification_hint.lean:12:9: warning: declaration 'cons_append_hint'' uses sorry
diff --git a/tests/lean/cls_err.lean b/tests/lean/cls_err.lean
index 050d86c169..c33b8ab57e 100644
--- a/tests/lean/cls_err.lean
+++ b/tests/lean/cls_err.lean
@@ -1,6 +1,6 @@
 --
 universe variables u
-inductive [class] H (A : Type u)
+class inductive H (A : Type u)
 | mk : A → H
 
 definition foo {A : Type u} [h : H A] : A :=
diff --git a/tests/lean/cmd_meta_errors.lean b/tests/lean/cmd_meta_errors.lean
new file mode 100644
index 0000000000..4b381c5873
--- /dev/null
+++ b/tests/lean/cmd_meta_errors.lean
@@ -0,0 +1,20 @@
+/-- docs -/
+run_cmd
+
+@[class]
+run_cmd
+
+private run_cmd
+
+meta axiom
+
+private protected def f := 42
+private private def f := 42
+
+private inductive
+protected inductive
+noncomputable inductive
+
+private instance
+protected instance
+mutual instance
diff --git a/tests/lean/cmd_meta_errors.lean.expected.out b/tests/lean/cmd_meta_errors.lean.expected.out
new file mode 100644
index 0000000000..3953906b4b
--- /dev/null
+++ b/tests/lean/cmd_meta_errors.lean.expected.out
@@ -0,0 +1,12 @@
+cmd_meta_errors.lean:2:0: error: command does not accept doc string
+cmd_meta_errors.lean:5:0: error: command does not accept attributes
+cmd_meta_errors.lean:7:8: error: command does not accept modifiers
+cmd_meta_errors.lean:9:5: error: invalid 'meta' modifier for axiom
+cmd_meta_errors.lean:11:8: error: unexpected definition modifier
+cmd_meta_errors.lean:12:8: error: unexpected definition modifier
+cmd_meta_errors.lean:14:0: error: invalid 'private' modifier for inductive type
+cmd_meta_errors.lean:15:0: error: invalid 'protected' modifier for inductive type
+cmd_meta_errors.lean:16:0: error: invalid 'noncomputable' modifier for inductive type
+cmd_meta_errors.lean:18:8: error: invalid 'private' modifier for instance command
+cmd_meta_errors.lean:19:10: error: invalid 'protected' modifier for instance command
+cmd_meta_errors.lean:20:7: error: invalid 'mutual' modifier for instance command
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index 3292e5d0b2..42b904d529 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -8,7 +8,7 @@ but is expected to have type
   ?m_1 → ?m_2 → ?m_4
 Additional information:
 elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
-elab_error_msgs.lean:4:0: warning: declaration 'bogus_elim' uses sorry
+elab_error_msgs.lean:5:0: warning: declaration 'bogus_elim' uses sorry
 elab_error_msgs.lean:9:0: error: type mismatch at application
   bogus_elim trivial
 term
diff --git a/tests/lean/hole_issue2.lean.expected.out b/tests/lean/hole_issue2.lean.expected.out
index b85b37bd08..e188053ff4 100644
--- a/tests/lean/hole_issue2.lean.expected.out
+++ b/tests/lean/hole_issue2.lean.expected.out
@@ -1,4 +1,4 @@
-hole_issue2.lean:12:0: warning: declaration 'count' uses sorry
+hole_issue2.lean:12:14: warning: declaration 'count' uses sorry
 hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
 context:
 A : Type,
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 1de8832268..a249771a54 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -1,6 +1,6 @@
 set_option pp.notation false
 
-inductive [class] C (A : Type*)
+class inductive C (A : Type*)
 | mk : A → C
 
 definition val {A : Type*} (c : C A) : A :=
diff --git a/tests/lean/run/class11.lean b/tests/lean/run/class11.lean
index e45990c683..62e77b14ab 100644
--- a/tests/lean/run/class11.lean
+++ b/tests/lean/run/class11.lean
@@ -1,4 +1,4 @@
-inductive [class] C {A : Type} : A → Prop
+class inductive C {A : Type} : A → Prop
 
 constant f {A : Type} (a : A) [H : C a] : Prop
 
diff --git a/tests/lean/run/imp3.lean b/tests/lean/run/imp3.lean
index c77cda007b..c413200b8d 100644
--- a/tests/lean/run/imp3.lean
+++ b/tests/lean/run/imp3.lean
@@ -1,4 +1,4 @@
-structure [class] is_equiv {A B : Type} (f : A → B) :=
+class is_equiv {A B : Type} (f : A → B) :=
   (inv : B → A)
 
 #check @is_equiv.inv
diff --git a/tests/lean/run/parent_struct_inst.lean b/tests/lean/run/parent_struct_inst.lean
index 09861bf5ff..94e9e4b080 100644
--- a/tests/lean/run/parent_struct_inst.lean
+++ b/tests/lean/run/parent_struct_inst.lean
@@ -1,6 +1,6 @@
 open nat
 
-structure [class] A := (n : ℕ)
+class A := (n : ℕ)
 
 definition f [A] := A.n
 
diff --git a/tests/lean/run/priority_test2.lean b/tests/lean/run/priority_test2.lean
index 48df160164..1b12b528fc 100644
--- a/tests/lean/run/priority_test2.lean
+++ b/tests/lean/run/priority_test2.lean
@@ -1,6 +1,6 @@
 open nat
 
-structure [class] foo :=
+class foo :=
 (a : nat) (b : nat)
 
 attribute [instance, priority std.priority.default-2]
diff --git a/tests/lean/run/record10.lean b/tests/lean/run/record10.lean
index e5168c0fcf..04b6d0dd62 100644
--- a/tests/lean/run/record10.lean
+++ b/tests/lean/run/record10.lean
@@ -4,12 +4,12 @@ set_option old_structure_cmd true
 
 #print "======================="
 
-structure [class] has_two_muls (A : Type) extends has_mul A renaming mul→mul1,
-                                          private has_mul A renaming mul→mul2
+class has_two_muls (A : Type) extends has_mul A renaming mul→mul1,
+                              private has_mul A renaming mul→mul2
 
 #print prefix has_two_muls
 
 #print "======================="
 
-structure [class] another_two_muls (A : Type) extends has_mul A renaming mul→mul1,
-                                                      has_mul A renaming mul→mul2
+class another_two_muls (A : Type) extends has_mul A renaming mul→mul1,
+                                          has_mul A renaming mul→mul2
diff --git a/tests/lean/run/section5.lean b/tests/lean/run/section5.lean
index fa6873b9ec..223aeacfab 100644
--- a/tests/lean/run/section5.lean
+++ b/tests/lean/run/section5.lean
@@ -5,7 +5,7 @@ section foo
 
   #check foo
 
-  structure [class] point :=
+  class point :=
   (x : A) (y : A)
 end foo
 
diff --git a/tests/lean/run/struc_names.lean b/tests/lean/run/struc_names.lean
index 97e9d4889e..9e35e71d5f 100644
--- a/tests/lean/run/struc_names.lean
+++ b/tests/lean/run/struc_names.lean
@@ -1,9 +1,9 @@
 namespace foo
 
-  structure [class] structA :=
+  class structA :=
   mk :: (a : nat)
 
-  structure [class] structB extends structA :=
+  class structB extends structA :=
   mk :: (b : nat)
 
   #check @structA.a
diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean
index 9477828ce0..5fed27ae57 100644
--- a/tests/lean/run/univ_bug1.lean
+++ b/tests/lean/run/univ_bug1.lean
@@ -10,7 +10,7 @@ namespace nsimp
 -- set_option pp.implicit true
 
 -- first define a class of homogeneous equality
-inductive [class] simplifies_to {T : Type} (t1 t2 : T) : Prop
+class inductive simplifies_to {T : Type} (t1 t2 : T) : Prop
 | mk : t1 = t2 → simplifies_to
 
 theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean
index 57827921df..3b7e3b8391 100644
--- a/tests/lean/run/univ_bug2.lean
+++ b/tests/lean/run/univ_bug2.lean
@@ -6,7 +6,7 @@
 open nat
 
 -- first define a class of homogeneous equality
-inductive [class] simplifies_to {T : Type} (t1 t2 : T) : Prop
+class inductive simplifies_to {T : Type} (t1 t2 : T) : Prop
 | mk : t1 = t2 → simplifies_to
 
 namespace simplifies_to
diff --git a/tests/lean/struct_class.lean b/tests/lean/struct_class.lean
index d25ab280d8..c4a0f17d38 100644
--- a/tests/lean/struct_class.lean
+++ b/tests/lean/struct_class.lean
@@ -1,7 +1,7 @@
 prelude
 import init.core
 
-structure [class] point (A : Type*) (B : Type*) :=
+class point (A : Type*) (B : Type*) :=
 mk :: (x : A) (y : B)
 
 #print classes
diff --git a/tests/lean/user_attribute.lean.expected.out b/tests/lean/user_attribute.lean.expected.out
index db299223f0..b861d243ec 100644
--- a/tests/lean/user_attribute.lean.expected.out
+++ b/tests/lean/user_attribute.lean.expected.out
@@ -7,11 +7,11 @@ eq.refl
 @[foo, foo.baz, refl]
 constructor eq.refl : ∀ {α : Sort u} (a : α), a = a
 [eq.refl]
-user_attribute.lean:22:0: error: an attribute named [reducible] has already been registered
-user_attribute.lean:22:0: warning: declaration 'duplicate' uses sorry
-user_attribute.lean:27:0: error: invalid [user_attribute], must be applied to definition of type user_attribute
+user_attribute.lean:23:0: error: an attribute named [reducible] has already been registered
+user_attribute.lean:23:0: warning: declaration 'duplicate' uses sorry
+user_attribute.lean:28:0: error: invalid [user_attribute], must be applied to definition of type user_attribute
 user_attribute.lean:28:11: error: don't know how to synthesize placeholder
 context:
 ⊢ Sort ?
-user_attribute.lean:33:2: error: invalid [user_attribute], must be applied to definition of type user_attribute
-user_attribute.lean:33:2: warning: declaration 'baz_attr' uses sorry
+user_attribute.lean:34:2: error: invalid [user_attribute], must be applied to definition of type user_attribute
+user_attribute.lean:34:2: warning: declaration 'baz_attr' uses sorry
diff --git a/tests/lean/user_notation.lean.expected.out b/tests/lean/user_notation.lean.expected.out
index dc3ffccd8f..d5eeb1d8ac 100644
--- a/tests/lean/user_notation.lean.expected.out
+++ b/tests/lean/user_notation.lean.expected.out
@@ -1,11 +1,11 @@
 2
 0 + (1 + 0) + (1 + 1) + (1 + 2) + (1 + 3) + (1 + 4) + (1 + 5) + (1 + 6) + (1 + 7) + (1 + 8) + (1 + 9) : ℕ
-user_notation.lean:21:0: error: invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.parse lean.parser.pexpr` parameter
+user_notation.lean:22:5: error: invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.parse lean.parser.pexpr` parameter
 user_notation.lean:22:9: error: don't know how to synthesize placeholder
 context:
 e₁ : parse lean.parser.pexpr
 ⊢ Sort ?
-user_notation.lean:24:0: error: invalid user-defined notation, must return type `lean.parser p`
+user_notation.lean:25:5: error: invalid user-defined notation, must return type `lean.parser p`
 user_notation.lean:25:9: error: don't know how to synthesize placeholder
 context:
 e₁ : parse (tk "(")