From 400aa435f36be45685ff8d4d6ec0f4e9aa5ea5c9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Jun 2020 15:43:46 -0700 Subject: [PATCH] fix: add missing precedence to `liftMethod` and remove unnecessary precedence from `doLet` --- 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 7642903cb9..adc19ce949 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -126,14 +126,14 @@ def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl @[builtinTermParser] def «let!» := parser! [leadPrec] "let! " >> letDecl >> "; " >> termParser def leftArrow : Parser := unicodeSymbol " ← " " <- " -def doLet := parser! [leadPrec] "let ">> letDecl +def doLet := parser! "let ">> letDecl def doId := parser! try (ident >> optType >> leftArrow) >> termParser def doPat := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser) def doExpr := parser! termParser def doElem := doLet <|> doId <|> doPat <|> doExpr def doSeq := sepBy1 doElem "; " def bracketedDoSeq := parser! [appPrec] "{" >> doSeq >> "}" -@[builtinTermParser] def liftMethod := parser! leftArrow >> termParser +@[builtinTermParser] def liftMethod := parser! [0] leftArrow >> termParser @[builtinTermParser] def «do» := parser! [leadPrec] "do " >> (bracketedDoSeq <|> doSeq) @[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser appPrec