max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add loop prenvention code at do-expander

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-13 15:46:47 -07:00
parent 1a2a089c28
commit 2384826933
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Do.lean
View file

@ -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 =>