fix(frontends/lean/definition_cmds): add aliases

src/frontends/lean/decl_util.cpp

@@ -10,6 +10,8 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "library/locals.h"
 #include "library/placeholder.h"
+#include "library/protected.h"
+#include "library/aliases.h"
 #include "library/scoped_ext.h"
 #include "library/tactic/elaborate.h"
 #include "frontends/lean/util.h"
@@ -264,6 +266,17 @@ environment add_local_ref(parser & p, environment const & env, name const & c_na
     return p.add_local_ref(env, c_name, ref);
 }
 
+environment add_alias(environment const & env, bool is_protected, name const & c_name, name const & c_real_name) {
+    if (c_name != c_real_name) {
+        if (is_protected)
+            return add_expr_alias_rec(env, get_protected_shortest_name(c_real_name), c_real_name);
+        else
+            return add_expr_alias_rec(env, c_name, c_real_name);
+    } else {
+        return env;
+    }
+}
+
 struct definition_info {
     name     m_prefix;
     bool     m_is_private{false};

src/frontends/lean/decl_util.h

@@ -71,6 +71,8 @@ void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<exp
 environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name,
                           buffer<name> const & lp_names, buffer<expr> const & var_params);
 
+/** \brief Add alias for new declaration. */
+environment add_alias(environment const & env, bool is_protected, name const & c_name, name const & c_real_name);
 
 /** \brief In Lean, declarations may contain nested definitions.
     This object is used to propagate relevant flags to

src/frontends/lean/definition_cmds.cpp

@@ -317,6 +317,8 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
     if (is_protected)
         new_env = add_protected(new_env, c_real_name);
 
+    new_env = add_alias(new_env, is_protected, c_name, c_real_name);
+
     if (!is_private) {
         p.add_decl_index(c_real_name, pos, p.get_cmd_token(), type);
         new_env = ensure_decl_namespaces(new_env, c_real_name);