diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index a32705ff2a..e21ac5a7cb 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -924,6 +924,28 @@ static expr parse_lparen(parser_state & p, unsigned, expr const *, pos_info cons
     }
 }
 
+static expr parse_lambda_cons(parser_state & p, unsigned, expr const *, pos_info const & pos) {
+    list<pair<transition, parse_table>> ts = p.led().find(get_dcolon_tk());
+    if (!ts || tail(ts) || !head(ts).second.is_accepting())
+        throw parser_error("invalid '(::)' notation, infix operator '::' has not been defined yet or is the prefix of another notation declaration", pos);
+    notation::action const & act = head(ts).first.get_action();
+    if (act.kind() != notation::action_kind::Expr)
+        throw parser_error("invalid '(::)' notation, declaration for operator '::' is not compatible with the `(::)` syntactic sugar", pos);
+    expr args[2];
+    buffer<expr> vars;
+    args[0] = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
+    vars.push_back(args[0]);
+    args[1] = mk_local(mk_fresh_name(), "_y", mk_expr_placeholder(), binder_info());
+    vars.push_back(args[1]);
+    buffer<expr> cs;
+    for (notation::accepting const & acc : head(ts).second.is_accepting()) {
+        expr r = p.copy_with_new_pos(acc.get_expr(), pos);
+        r = p.save_pos(mk_infix_function(Fun(vars, instantiate_rev(r, 2, args), p)), pos);
+        cs.push_back(r);
+    }
+    return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -947,6 +969,7 @@ parse_table init_nud_table() {
     r = r.add({transition("%%", mk_ext_action(parse_antiquote_expr))}, x0);
     r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);
     r = r.add({transition("()", mk_ext_action(parse_unit))}, x0);
+    r = r.add({transition("(::)", mk_ext_action(parse_lambda_cons))}, x0);
     r = r.add({transition("fun", mk_ext_action(parse_lambda))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index d7b417545e..27ea7a4724 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -83,7 +83,7 @@ void init_token_table(token_table & t) {
          {"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
          {"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"``(", g_max_prec},
          {"```(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec},
-         {"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0},
+         {"%%", g_max_prec}, {"()", g_max_prec}, {"(::)", g_max_prec}, {")", 0}, {"'", 0},
          {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
          {"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
diff --git a/tests/lean/run/lambda_cons.lean b/tests/lean/run/lambda_cons.lean
new file mode 100644
index 0000000000..31e1eba83a
--- /dev/null
+++ b/tests/lean/run/lambda_cons.lean
@@ -0,0 +1 @@
+#eval list.foldr (::) [] [1, 2, 3]