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

fix: indent where definitions and add space before

Browse source
This commit is contained in:
Gabriel Ebner 2021-12-08 21:48:24 +01:00 • committed by Sebastian Ullrich
parent f5a2562575
commit e90bdd00db
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

@ -55,7 +55,7 @@ def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithou
def declValSimple := leading_parser " :=\n" >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser Term.matchAltsWhereDecls
def whereStructField := leading_parser Term.letDecl
def whereStructInst := leading_parser "where " >> many1Indent (group (whereStructField >> optional ";"))
def whereStructInst := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (whereStructField >> optional ";")))
/-
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

@ -209,7 +209,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" >> many1Indent (ppLine >> group (letRecDecl >> optional ";"))
def whereDecls := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (letRecDecl >> optional ";")))
@[runBuiltinParserAttributeHooks]
def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls