From d618bf5b16994f9d5a263f0d8bca088f0ae388fd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Nov 2020 07:22:38 -0800 Subject: [PATCH] feat: expand new `syntax` Syntax --- src/Lean/Elab/Syntax.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index caf79afa37..e489341de3 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -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)