feat: add let_expr notation

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

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

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