From cc34733e520245b050259b8b800992fc5d5bdcc4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Dec 2020 11:50:32 -0800 Subject: [PATCH] fix: update builtin precedences for `|>.` and `macroDollarArg` --- src/Lean/Parser/Term.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 1c0b16a814..8230071fd1 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -195,7 +195,7 @@ def isIdent (stx : Syntax) : Bool := @[builtinTermParser] def explicitUniv : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}" @[builtinTermParser] def namedPattern : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec -@[builtinTermParser] def pipeProj := tparser!:0 " |>. " >> (fieldIdx <|> ident) +@[builtinTermParser] def pipeProj := tparser!:10 " |>. " >> (fieldIdx <|> ident) @[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ " @@ -211,7 +211,7 @@ def isIdent (stx : Syntax) : Bool := @[builtinTermParser] def assert := parser!:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser def macroArg := termParser maxPrec -def macroDollarArg := parser! "$" >> termParser 0 +def macroDollarArg := parser! "$" >> termParser 10 def macroLastArg := macroDollarArg <|> macroArg -- Macro for avoiding exponentially big terms when using `STWorld`