feat: add dummy elabForIn

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

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;

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