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

feat: expand new syntax Syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-08 07:22:38 -08:00
parent 1171590d2e
commit d618bf5b16
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Elab/Syntax.lean
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)