diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 1385f91e89..439143cf65 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -216,6 +216,17 @@ def binderTactic := leading_parser atomic (symbol " := " >> " by ") >> Tactic.tacticSeq def binderDefault := leading_parser " := " >> termParser + +open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in +@[combinator_parenthesizer Lean.Parser.Term.binderDefault] def binderDefault.parenthesizer : Parenthesizer := do + let prec := match (← getCur) with + -- must parenthesize to distinguish from `binderTactic` + | `(binderDefault| := by $_) => maxPrec + | _ => 0 + visitArgs do + term.parenthesizer prec + visitToken + def explicitBinder (requireType := false) := ppGroup $ leading_parser "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")" /-- diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean index 8e62ffb0dd..1683203355 100644 --- a/tests/lean/run/Reparen.lean +++ b/tests/lean/run/Reparen.lean @@ -51,3 +51,4 @@ open Lean syntax:80 term " ^~ " term:80 : term syntax:70 term " *~ " term:71 : term #eval check $ Unhygienic.run `(((1 + 2) *~ 3) ^~ 4) +#eval check $ Unhygienic.run `(opaque foo (a := (by exact 1)) : True)