diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 3b0fceeac6..37bb9dac35 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -262,7 +262,7 @@ def macroLastArg := macroDollarArg <|> macroArg @[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")" -@[builtinTermParser] def «if» := leading_parser:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser +@[builtinTermParser] def «if» := leading_parser:leadPrec ppGroup $ ppDedent $ "if " >> optIdent >> termParser >> " then" >> ppSpace >> termParser >> ppDedent (ppSpace >> "else") >> ppSpace >> termParser end Term