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

chore: add TODO

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-06 19:12:08 -07:00
parent 294a750110
commit 2fda7f4f9f
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -934,6 +934,8 @@ unit ← `(PUnit.unit);
let unit := unit.copyInfo ref;
pure $ mkReturn ref unit
-- TODO: we must expand macros occurring in patterns before invoking getPatternVars
partial def doSeqToCode : List Syntax → M CodeBlock
| [] => do ctx ← read; mkReturnUnit ctx.ref
| doElem::doElems => withRef doElem do