From a3c0e2bb36cb9c58b801c87536d3cbea194b3649 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 Jul 2019 08:26:42 -0700
Subject: [PATCH] chore(frontends/lean/builtin_exprs): ensure old `let`
 notation is not accepted

---
 src/frontends/lean/builtin_exprs.cpp | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index a00bb9b71a..2a5a350b66 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -91,14 +91,11 @@ static expr parse_let(parser & p, pos_info const & pos, bool in_do_block);
 static expr parse_do(parser & p, bool has_braces);
 static expr parse_let_body(parser & p, pos_info const & pos, bool in_do_block) {
     if (in_do_block) {
-        if (p.curr_is_token(get_in_tk())) {
-            p.next();
-            return p.parse_expr();
-        } else {
-            if (p.curr_is_token(get_semicolon_tk()) || p.curr_is_token(get_comma_tk())) {
+        {
+            if (p.curr_is_token(get_semicolon_tk())) {
                 p.next();
             } else {
-                p.check_token_next(get_semicolon_tk(), "invalid 'do' block 'let' declaration, ',', ';' or 'in' expected");
+                p.check_token_next(get_semicolon_tk(), "invalid 'do' block 'let' declaration, ';' expected");
             }
             if (p.curr_is_token(get_let_tk())) {
                 p.next();
@@ -108,11 +105,11 @@ static expr parse_let_body(parser & p, pos_info const & pos, bool in_do_block) {
             }
         }
     } else {
-        if (p.curr_is_token(get_in_tk()) || p.curr_is_token(get_semicolon_tk())) {
+        if (p.curr_is_token(get_semicolon_tk())) {
             p.next();
             return p.parse_expr();
         } else {
-            p.maybe_throw_error({"invalid let declaration, 'in' or ';' expected", p.pos()});
+            p.maybe_throw_error({"invalid let declaration, ';' expected", p.pos()});
             return p.parse_expr();
         }
     }
@@ -656,7 +653,7 @@ static expr parse_lambda_binder(parser & p, pos_info const & pos) {
     } else if (p.curr_is_token(get_langle_tk())) {
         body = parse_lambda_core(p, pos);
     } else {
-        p.maybe_throw_error({"invalid lambda expression, ',', '=>' or '⟨' expected", p.pos()});
+        p.maybe_throw_error({"invalid lambda expression, '=>' or '⟨' expected", p.pos()});
         body = p.parse_expr();
     }
     return p.rec_save_pos(Fun(locals, body, p), pos);
@@ -674,7 +671,7 @@ static expr parse_lambda_constructor(parser & p, pos_info const & ini_pos) {
     for (expr const & local : locals)
         p.add_local(local);
     expr body;
-    if (/* p.curr_is_token(get_comma_tk()) || */ p.curr_is_token(get_darrow_tk())) {
+    if (p.curr_is_token(get_darrow_tk())) {
         p.next();
         body = p.parse_expr();
     } else {