From 3e7d45aaba7e5e91ba72d0f0b4ecb697c23ed648 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 Jul 2022 18:18:05 -0700
Subject: [PATCH] fix: improve finer-grained term infos for `do` blocks
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

see #1248

This commit adds a small hack to fix the term info for the following `do`-elements
```lean
   let (x, y) := ...
   let (x, y) ← ...
   let mut (x, y) ← ...
   let some x ← ... | ...
```
---
 src/Lean/Elab/Do.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 3cf8328970..d01783d71d 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1312,16 +1312,16 @@ mutual
       let optElse := decl[3]
       if optElse.isNone then withFreshMacroScope do
         let auxDo ← if isMutableLet doLetArrow then
-          `(do let discr ← $doElem; let mut $pattern:term := discr)
+          `(do let%$doLetArrow discr ← $doElem; let%$doLetArrow mut $pattern:term := discr)
         else
-          `(do let discr ← $doElem; let $pattern:term := discr)
+          `(do let%$doLetArrow discr ← $doElem; let%$doLetArrow $pattern:term := discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         if isMutableLet doLetArrow then
           throwError "`mut` is currently not supported in let-decls with `else` case"
         let contSeq := mkDoSeq doElems.toArray
         let elseSeq := mkSingletonDoSeq optElse[1]
-        let auxDo ← `(do let discr ← $doElem; match discr with | $pattern:term => $contSeq | _ => $elseSeq)
+        let auxDo ← `(do let%$doLetArrow discr ← $doElem; match%$doLetArrow discr with | $pattern:term => $contSeq | _ => $elseSeq)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
     else
       throwError "unexpected kind of `do` declaration"