From 63e982768a93a87bc5cb08c565600c8115a68185 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Oct 2020 17:11:50 -0700
Subject: [PATCH] feat: expand nested `do`s

---
 src/Lean/Elab/Do.lean        |  3 +++
 tests/lean/run/nestedDo.lean | 11 +++++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 tests/lean/run/nestedDo.lean

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index d851971323..c76db8e9dc 100644
--- a/src/Lean/Elab/Do.lean
+++ b/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
diff --git a/tests/lean/run/nestedDo.lean b/tests/lean/run/nestedDo.lean
new file mode 100644
index 0000000000..e4a2b66949
--- /dev/null
+++ b/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