diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 8a94d166de..d2e0595b58 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -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`. diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 88eec8ff87..cd0434a87e 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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