diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 2a5e56996..3f2fb9ba5 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -22,7 +22,7 @@
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing"
     "calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "Pi" "fun"
     "exists" "if" "dif" "then" "else" "assume" "assert" "take"
-    "obtain" "from")
+    "obtain" "from" "aliases")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean-keywords1-regexp
   (eval `(rx word-start (or ,@lean-keywords1) word-end)))
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 3b411a978..944b82d65 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -595,6 +595,19 @@ static void print_no_patterns(parser & p) {
     out << "\n";
 }
 
+static void print_aliases(parser const & p) {
+    io_state_stream out = p.regular_stream();
+    for_each_expr_alias(p.env(), [&](name const & n, list<name> const & as) {
+            out << n << " -> {";
+            bool first = true;
+            for (name const & a : as) {
+                if (first) first = false; else out << ", ";
+                out << a;
+            }
+            out << "}\n";
+        });
+}
+
 environment print_cmd(parser & p) {
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
@@ -676,6 +689,9 @@ environment print_cmd(parser & p) {
     } else if (p.curr_is_token_or_id(get_prefix_tk())) {
         p.next();
         print_prefix(p);
+    } else if (p.curr_is_token_or_id(get_aliases_tk())) {
+        p.next();
+        print_aliases(p);
     } else if (p.curr_is_token_or_id(get_coercions_tk())) {
         p.next();
         optional<name> C;
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index b00a376a3..3173895af 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -3,6 +3,7 @@
 // DO NOT EDIT, automatically generated file, generator scripts/gen_tokens_cpp.py
 #include "util/name.h"
 namespace lean{
+static name const * g_aliases_tk = nullptr;
 static name const * g_period_tk = nullptr;
 static name const * g_placeholder_tk = nullptr;
 static name const * g_colon_tk = nullptr;
@@ -163,6 +164,7 @@ static name const * g_this_tk = nullptr;
 static name const * g_noncomputable_tk = nullptr;
 static name const * g_theory_tk = nullptr;
 void initialize_tokens() {
+    g_aliases_tk = new name{"aliases"};
     g_period_tk = new name{"."};
     g_placeholder_tk = new name{"_"};
     g_colon_tk = new name{":"};
@@ -324,6 +326,7 @@ void initialize_tokens() {
     g_theory_tk = new name{"theory"};
 }
 void finalize_tokens() {
+    delete g_aliases_tk;
     delete g_period_tk;
     delete g_placeholder_tk;
     delete g_colon_tk;
@@ -484,6 +487,7 @@ void finalize_tokens() {
     delete g_noncomputable_tk;
     delete g_theory_tk;
 }
+name const & get_aliases_tk() { return *g_aliases_tk; }
 name const & get_period_tk() { return *g_period_tk; }
 name const & get_placeholder_tk() { return *g_placeholder_tk; }
 name const & get_colon_tk() { return *g_colon_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index c2a506ef7..d07e2a934 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -5,6 +5,7 @@
 namespace lean {
 void initialize_tokens();
 void finalize_tokens();
+name const & get_aliases_tk();
 name const & get_period_tk();
 name const & get_placeholder_tk();
 name const & get_colon_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 7736dc3d0..645284ae6 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -1,3 +1,4 @@
+aliases      aliases
 period       .
 placeholder  _
 colon        :