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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-15 17:13:09 -07:00
parent 63e982768a
commit e754d7cc4e
2 changed files with 2798 additions and 2726 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1451,6 +1451,9 @@ partial def doSeqToCode : List Syntax → M CodeBlock
mkSeq doElem <$> doSeqToCode doElems
else if k == `Lean.Parser.Term.doAssert then
mkSeq doElem <$> doSeqToCode doElems
else if k == `Lean.Parser.Term.doNested then
let nestedDoSeq := doElem[1]
doSeqToCode (getDoSeqElems nestedDoSeq ++ doElems)
else if k == `Lean.Parser.Term.doExpr then
let term := doElem[0]
if doElems.isEmpty then

5521
stage0/stdlib/Lean/Elab/Do.c generated
View file

File diff suppressed because it is too large Load diff