diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 8290d2f17..706667023 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/let.h"
+#include "library/definitional/equations.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
@@ -507,7 +508,8 @@ parse_table init_nud_table() {
 
 parse_table init_led_table() {
     parse_table r(false);
-    r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(1), Var(1)));
+    r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))},    mk_arrow(Var(1), Var(1)));
+    r = r.add({transition("<d", mk_expr_action(get_decreasing_prec()))}, mk_decreasing(Var(1), Var(0)));
     return r;
 }
 }
diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp
index 902c51b2b..0c288a71e 100644
--- a/src/frontends/lean/init_module.cpp
+++ b/src/frontends/lean/init_module.cpp
@@ -32,6 +32,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 void initialize_frontend_lean_module() {
+    initialize_info_annotation();
     initialize_tokens();
     initialize_token_table();
     initialize_parse_table();
@@ -42,7 +43,6 @@ void initialize_frontend_lean_module() {
     initialize_pp_options();
     initialize_scanner();
     initialize_parser();
-    initialize_info_annotation();
     initialize_tactic_hint();
     initialize_class();
     initialize_parser_config();
@@ -73,7 +73,6 @@ void finalize_frontend_lean_module() {
     finalize_parser_config();
     finalize_class();
     finalize_tactic_hint();
-    finalize_info_annotation();
     finalize_parser();
     finalize_scanner();
     finalize_pp_options();
@@ -84,5 +83,6 @@ void finalize_frontend_lean_module() {
     finalize_parse_table();
     finalize_token_table();
     finalize_tokens();
+    finalize_info_annotation();
 }
 }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 728834623..28ae6f39c 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -10,12 +10,14 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 
 namespace lean {
-static unsigned g_arrow_prec = 25;
-static unsigned g_max_prec   = 1024;
-static unsigned g_plus_prec  = 65;
-static unsigned g_cup_prec   = 60;
+static unsigned g_arrow_prec      = 25;
+static unsigned g_decreasing_prec = 25;
+static unsigned g_max_prec        = 1024;
+static unsigned g_plus_prec       = 65;
+static unsigned g_cup_prec        = 60;
 unsigned get_max_prec() { return g_max_prec; }
 unsigned get_arrow_prec() { return g_arrow_prec; }
+unsigned get_decreasing_prec() { return g_decreasing_prec; }
 token_table add_command_token(token_table const & s, char const * token) {
     return insert(s, token, token_info(token));
 }
@@ -60,12 +62,13 @@ void display(std::ostream & out, token_table const & s) {
         });
 }
 
-static char const * g_lambda_unicode = "\u03BB";
-static char const * g_pi_unicode     = "\u03A0";
-static char const * g_forall_unicode = "\u2200";
-static char const * g_arrow_unicode  = "\u2192";
-static char const * g_cup            = "\u2294";
-static char const * g_qed_unicode    = "∎";
+static char const * g_lambda_unicode     = "\u03BB";
+static char const * g_pi_unicode         = "\u03A0";
+static char const * g_forall_unicode     = "\u2200";
+static char const * g_arrow_unicode      = "\u2192";
+static char const * g_cup                = "\u2294";
+static char const * g_qed_unicode        = "∎";
+static char const * g_decreasing_unicode = "↓";
 
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
@@ -76,8 +79,8 @@ void init_token_table(token_table & t) {
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
-         {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0},
-         {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
+         {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
+         {"<d", g_decreasing_prec}, {"local", 0}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
@@ -116,6 +119,7 @@ void init_token_table(token_table & t) {
         it3++;
     }
     t = add_token(t, g_arrow_unicode, "->", get_arrow_prec());
+    t = add_token(t, g_decreasing_unicode, "<d", get_decreasing_prec());
 
     auto it4 = cmd_aliases;
     while (it4->first) {
diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h
index 2fef36766..10f0beb3c 100644
--- a/src/frontends/lean/token_table.h
+++ b/src/frontends/lean/token_table.h
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 namespace lean {
 unsigned get_max_prec();
 unsigned get_arrow_prec();
+unsigned get_decreasing_prec();
 class token_info {
     bool        m_command;
     name        m_token;