diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index c65d631fa..5a72f13f4 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/abstract.h"
 #include "library/placeholder.h"
+#include "library/explicit.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
@@ -264,6 +265,11 @@ static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_inf
     return p.parse_scoped_expr(0, nullptr, env);
 }
 
+static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    expr e = p.parse_expr(get_max_prec());
+    return p.save_pos(mk_explicit(e), pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -281,6 +287,7 @@ parse_table init_nud_table() {
     r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
+    r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
     return r;
 }
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 8ba5af18b..3fbdffc8b 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -13,6 +13,7 @@ static unsigned g_arrow_prec = 25;
 static unsigned g_max_prec   = std::numeric_limits<unsigned>::max();
 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; }
 token_table add_command_token(token_table const & s, char const * token) {
     return insert(s, token, token_info(token));
@@ -58,7 +59,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
          {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0},
+         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", 0},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition",
diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h
index 881131ce0..17090d7c8 100644
--- a/src/frontends/lean/token_table.h
+++ b/src/frontends/lean/token_table.h
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 
 namespace lean {
+unsigned get_max_prec();
 unsigned get_arrow_prec();
 class token_info {
     bool        m_command;