From 2d6b59f4bbc5873426f8f46239f662cf062b8952 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Feb 2021 17:02:11 -0800
Subject: [PATCH] feat: add dummy `elabForIn`

---
 src/Lean/Elab.lean       |  1 +
 src/Lean/Elab/Do.lean    |  4 ++--
 src/Lean/Elab/Extra.lean | 19 +++++++++++++++++++
 3 files changed, 22 insertions(+), 2 deletions(-)
 create mode 100644 src/Lean/Elab/Extra.lean

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 5f5495ee35..5e8a751bec 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -27,3 +27,4 @@ import Lean.Elab.MutualDef
 import Lean.Elab.PreDefinition
 import Lean.Elab.Deriving
 import Lean.Elab.DeclarationRange
+import Lean.Elab.Extra
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 88cfb13142..7248cff342 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1354,7 +1354,7 @@ mutual
       let uvarsTuple ← liftMacroM do mkTuple (← uvars.mapM mkIdentFromRef)
       if hasReturn forInBodyCodeBlock.code then
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ← `(forIn (m := $((← read).m)) $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
+        let forInTerm ← `(forIn! $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
         let auxDo ← `(do let r ← $forInTerm:term;
                          $uvarsTuple:term := r.2;
                          match r.1 with
@@ -1363,7 +1363,7 @@ mutual
         doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
       else
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ← `(forIn (m := $((← read).m)) $(xs) $uvarsTuple fun $x r => $forInBody)
+        let forInTerm ← `(forIn! $(xs) $uvarsTuple fun $x r => $forInBody)
         if doElems.isEmpty then
           let auxDo ← `(do let r ← $forInTerm:term;
                            $uvarsTuple:term := r;
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
new file mode 100644
index 0000000000..05954d92cf
--- /dev/null
+++ b/src/Lean/Elab/Extra.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Term
+
+/-
+Auxiliary elaboration functions: AKA custom elaborators
+-/
+
+namespace Lean.Elab.Term
+
+@[builtinTermElab forInMacro] def elabForIn : TermElab :=  fun stx expectedType? => do
+  match stx with
+  | `(forIn! $c $e $body) => elabTerm (← `(forIn $c $e $body)) expectedType?
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Term