feat: add let pat := val | elseCase do-notation

src/Lean/Elab/Do.lean

@@ -1307,6 +1307,14 @@ mutual
     else
       throwError "unexpected kind of 'do' declaration"
 
+  partial def doLetElseToCode (doLetElse : Syntax) (doElems : List Syntax) : M CodeBlock := do
+    -- "let " >> termParser >> " := " >> termParser >> checkColGt >> " | " >> doElemParser
+    let pattern := doLetElse[1]
+    let val     := doLetElse[3]
+    let elseSeq := mkSingletonDoSeq doLetElse[5]
+    let contSeq := mkDoSeq doElems.toArray
+    let auxDo ← `(do let discr := $val; match discr with | $pattern:term => $contSeq | _ => $elseSeq)
+    doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
 
   /- Generate `CodeBlock` for `doReassignArrow; doElems`
      `doReassignArrow` is of the form
@@ -1550,6 +1558,8 @@ mutual
             mkReassignCore vars doElem k
           else if k == ``Lean.Parser.Term.doLetArrow then
             doLetArrowToCode doElem doElems
+          else if k == ``Lean.Parser.Term.doLetElse then
+            doLetElseToCode doElem doElems
           else if k == ``Lean.Parser.Term.doReassignArrow then
             doReassignArrowToCode doElem doElems
           else if k == ``Lean.Parser.Term.doIf then

src/Lean/Parser/Do.lean

@@ -37,6 +37,7 @@ def notFollowedByRedefinedTermToken :=
   notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
 
 @[builtinDoElemParser] def doLet      := leading_parser "let " >> optional "mut " >> letDecl
+@[builtinDoElemParser] def doLetElse  := leading_parser "let " >> termParser >> " := " >> termParser >> checkColGt >> " | " >> doElemParser
 
 @[builtinDoElemParser] def doLetRec   := leading_parser group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
 def doIdDecl   := leading_parser atomic (ident >> optType >> ppSpace >> leftArrow) >> doElemParser

tests/lean/run/doLetElse.lean

@@ -0,0 +1,12 @@
+def foo (x? : Option Nat) : IO Nat := do
+  let some x := x? | return 0
+  IO.println s!"x: {x}"
+  return x
+
+def test (input : Option Nat) (expected : Nat) : IO Unit := do
+  assert! (← foo input) == expected
+
+
+#eval test (some 10) 10
+#eval test none 0
+#eval test (some 1) 1