From 95742ca17bfbb51eae5022582ee670de37119dab Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 20 Aug 2020 18:09:33 +0200 Subject: [PATCH] fix: parenthesizer: take minimum of successive precedence checks for `contPrec` as well Otherwise, we would parenthesize `1 + 2 + 3` as `(1 + 2) + 3` since in ``` @[builtinTermParser] def add := tparser! infixL " + " 65 ``` there is an additional `checkPrec 1024` implied by `tparser!`. Now `contPrec` of this parser is (min 1024 65 = 65). --- src/Lean/PrettyPrinter/Parenthesizer.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 68847f876b..7c280af2f8 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -167,7 +167,7 @@ instance ParenthesizerM.monadTraverser : Syntax.MonadTraverser ParenthesizerM := open Syntax.MonadTraverser def addPrecCheck (prec : Nat) : ParenthesizerM Unit := -modify $ fun st => { st with contPrec := prec, minPrec := Nat.min (st.minPrec.getD prec) prec } +modify $ fun st => { st with contPrec := Nat.min (st.contPrec.getD prec) prec, minPrec := Nat.min (st.minPrec.getD prec) prec } /-- Execute `x` at the right-most child of the current node, if any, then advance to the left. -/ def visitArgs (x : ParenthesizerM Unit) : ParenthesizerM Unit := do