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

chore: provide ambient monad to forIn

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-04 18:31:28 -08:00
parent 53539b1dff
commit 3d4bc9f991
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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 $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
let forInTerm ← `(forIn (m := $((← read).m)) $(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 $(xs) $uvarsTuple fun $x r => $forInBody)
let forInTerm ← `(forIn (m := $((← read).m)) $(xs) $uvarsTuple fun $x r => $forInBody)
if doElems.isEmpty then
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r;