From 327717ade82c675fb62f26edd8f6ec456e6cf4e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Mar 2021 09:08:35 -0800 Subject: [PATCH] chore: add `leading_parser` and `trailing_parser` notation It will replace `parser!` and `tparser!` --- src/Lean/Parser/Term.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index faebac8c35..a832ab103e 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -147,6 +147,9 @@ def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun def optExprPrecedence := optional (atomic ":" >> termParser maxPrec) @[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser @[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser +@[builtinTermParser] def «leading_parser» := parser!:leadPrec "leading_parser " >> optExprPrecedence >> termParser +@[builtinTermParser] def «trailing_parser» := parser!:leadPrec "trailing_parser " >> optExprPrecedence >> termParser + @[builtinTermParser] def borrowed := parser! "@&" >> termParser leadPrec @[builtinTermParser] def quotedName := parser! nameLit @[builtinTermParser] def doubleQuotedName := parser! "`" >> checkNoWsBefore >> nameLit