max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add pp annotations to if parser

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-30 20:40:02 -07:00
parent 2aa190ec6a
commit 7c0993ae12
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Term.lean
View file

@ -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