From ecfaf8f3e7a3ddf7714b85148262d59bedc7aadd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 2 Mar 2024 07:26:29 -0800
Subject: [PATCH] feat: add `let_expr` notation

---
 src/Lean/Parser/Do.lean        | 12 +++++++++++-
 src/Lean/Parser/Term.lean      |  3 +++
 tests/lean/run/match_expr.lean | 18 ++++++++++++++++++
 3 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 29fdd2a9f4..3d648ac1bc 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -60,6 +60,14 @@ def notFollowedByRedefinedTermToken :=
   "let " >> optional "mut " >> termParser >> " := " >> termParser >>
   checkColGt >> " | " >> doSeq
 
+@[builtin_doElem_parser] def doLetExpr  := leading_parser
+  "let_expr " >> matchExprPat >> " := " >> termParser >>
+  checkColGt >> " | " >> doSeq
+
+@[builtin_doElem_parser] def doLetMetaExpr  := leading_parser
+  "let_expr " >> matchExprPat >> " ← " >> termParser >>
+  checkColGt >> " | " >> doSeq
+
 @[builtin_doElem_parser] def doLetRec   := leading_parser
   group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
 def doIdDecl   := leading_parser
@@ -151,8 +159,10 @@ def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
   sepBy1 matchDiscr ", " >> " with" >> doMatchAlts
 
 def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
+def optMetaFalse :=
+  optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ")
 @[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
-  "match_expr " >> optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ") >> termParser >> " with" >> doMatchExprAlts
+  "match_expr " >> optMetaFalse >> termParser >> " with" >> doMatchExprAlts
 
 def doCatch      := leading_parser
   ppDedent ppLine >> atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 772cfd6f77..0fc9514dc1 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -836,6 +836,9 @@ def matchExprAlts (rhsParser : Parser) :=
 @[builtin_term_parser] def matchExpr := leading_parser:leadPrec
   "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
 
+@[builtin_term_parser] def letExpr := leading_parser:leadPrec
+  withPosition ("let_expr " >> matchExprPat >> " := " >> termParser >> checkColGt >> " | " >> termParser) >> optSemicolon termParser
+
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser
diff --git a/tests/lean/run/match_expr.lean b/tests/lean/run/match_expr.lean
index 9c599b720e..55ece46454 100644
--- a/tests/lean/run/match_expr.lean
+++ b/tests/lean/run/match_expr.lean
@@ -54,3 +54,21 @@ run_meta do
   discard <| isDefEq m e
   let m ← test2 m
   logInfo m
+
+def test3 (e : Expr) : Option Expr :=
+  let_expr c@Eq α a b := e | none
+  some (mkApp3 c α b a)
+
+def test4 (e : Expr) : Option Expr :=
+  let_expr Eq.refl _ α := e | none
+  some a
+
+def test5 (e : Expr) : MetaM Expr := do
+  let_expr HAdd.hAdd _ _ _ _ a b ← e
+    | return e
+  mkSub a b
+
+def test6 (e : Expr) : MetaM Expr := do
+  let_expr HAdd.hAdd _ _ _ _ a b := e
+    | return e
+  mkSub a b