feat: expand nested dos

src/Lean/Elab/Do.lean

@@ -1451,6 +1451,9 @@ partial def doSeqToCode : List Syntax → M CodeBlock
       mkSeq doElem <$> doSeqToCode doElems
     else if k == `Lean.Parser.Term.doAssert then
       mkSeq doElem <$> doSeqToCode doElems
+    else if k == `Lean.Parser.Term.doNested then
+      let nestedDoSeq := doElem[1]
+      doSeqToCode (getDoSeqElems nestedDoSeq ++ doElems)
     else if k == `Lean.Parser.Term.doExpr then
       let term := doElem[0]
       if doElems.isEmpty then

tests/lean/run/nestedDo.lean

@@ -0,0 +1,11 @@
+#lang lean4
+
+def f (x : Nat) : StateM Nat Nat := do
+let y ← do
+  modify (·+1)
+  let s ← get
+  pure $ s + x
+pure $ y + 1
+
+theorem ex1 : (f 5).run' 2 = 9 :=
+rfl