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