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

chore: remove unnecessary ppLine

Browse source
This commit is contained in:
Gabriel Ebner 2022-06-23 22:06:59 +02:00 • committed by Sebastian Ullrich
parent 233a787e65
commit ec4200fc75
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -60,7 +60,7 @@ def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithou
def declValSimple := leading_parser " :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser Term.matchAltsWhereDecls
def whereStructField := leading_parser Term.letDecl
def whereStructInst := leading_parser " where" >> sepBy1Indent (ppLine >> ppGroup (whereStructField)) "; " (allowTrailingSep := true) >> optional Term.whereDecls
def whereStructInst := leading_parser " where" >> sepBy1Indent (ppGroup whereStructField) "; " (allowTrailingSep := true) >> optional Term.whereDecls
/-
Remark: we should not use `Term.whereDecls` at `declVal` because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes.
Issue #753 showns an example that fails to be parsed when we used `Term.whereDecls`.

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

@ -224,7 +224,7 @@ def letRecDecls := leading_parser sepBy1 letRecDecl ", "
def «letrec» := leading_parser:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser
@[runBuiltinParserAttributeHooks]
def whereDecls := leading_parser " where" >> sepBy1Indent (ppLine >> ppGroup letRecDecl) "; " (allowTrailingSep := true)
def whereDecls := leading_parser " where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true)
@[runBuiltinParserAttributeHooks]
def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls