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-11-08 07:24:20 -08:00
parent d618bf5b16
commit c03b98e46e
2 changed files with 4783 additions and 4001 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -131,6 +131,13 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := do
else if kind == `Lean.Parser.Syntax.try then
let d ← withoutLeftRec $ toParserDescrAux stx[1]
`(ParserDescr.try $d)
else if kind == `Lean.Parser.Syntax.withPosition then
let d ← withoutLeftRec $ toParserDescrAux stx[1]
`(ParserDescr.withPosition $d)
else if kind == `Lean.Parser.Syntax.checkColGt then
`(ParserDescr.checkCol true)
else if kind == `Lean.Parser.Syntax.checkColGe then
`(ParserDescr.checkCol false)
else if kind == `Lean.Parser.Syntax.notFollowedBy then
let d ← withoutLeftRec $ toParserDescrAux stx[1]
`(ParserDescr.notFollowedBy $d)

8777
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

File diff suppressed because it is too large Load diff