From 2384826933593c5ddaa787c3708f4193414f088e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Apr 2021 15:46:47 -0700 Subject: [PATCH] chore: add loop prenvention code at do-expander --- src/Lean/Elab/Do.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index a62cd4143b..f254f0f4d9 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -1451,7 +1451,8 @@ mutual partial def doSeqToCode : List Syntax → M CodeBlock | [] => do liftMacroM mkPureUnitAction - | doElem::doElems => withRef doElem do + | doElem::doElems => withIncRecDepth <| withRef doElem do + checkMaxHeartbeats "'do'-expander" match (← liftMacroM <| expandMacro? doElem) with | some doElem => doSeqToCode (doElem::doElems) | none =>