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

fix: indenting of match arms in declValEqns

Browse source
This commit is contained in:
Gabriel Ebner 2021-12-09 15:31:15 +01:00 • committed by Sebastian Ullrich
parent 067c181075
commit 5d25df1a69
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -94,7 +94,7 @@ def doIfCond := withAntiquot (mkAntiquot "doIfCond" none (anonymous := false)
def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
@[builtinDoElemParser] def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
def doMatchAlts := matchAlts (rhsParser := doSeq)
def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
@[builtinDoElemParser] def doMatch := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
def doCatch := leading_parser atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq

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

@ -20,7 +20,7 @@ builtin_initialize
def matchRhs := Term.hole <|> Term.syntheticHole <|> tacticSeq
def matchAlts := Term.matchAlts (rhsParser := matchRhs)
@[builtinTacticParser] def «match» := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
@[builtinTacticParser] def «match» := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> ppDedent matchAlts
@[builtinTacticParser] def introMatch := leading_parser nonReservedSymbol "intro " >> matchAlts
@[builtinTacticParser] def decide := leading_parser nonReservedSymbol "decide"

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

@ -133,7 +133,7 @@ def matchAlt (rhsParser : Parser := termParser) : Parser :=
def matchAltExpr := matchAlt
def matchAlts (rhsParser : Parser := termParser) : Parser :=
leading_parser ppDedent $ withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
def matchDiscr := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
@ -141,7 +141,7 @@ def trueVal := leading_parser nonReservedSymbol "true"
def falseVal := leading_parser nonReservedSymbol "false"
def generalizingParam := leading_parser atomic ("(" >> nonReservedSymbol "generalizing") >> " := " >> (trueVal <|> falseVal) >> ")"
@[builtinTermParser] def «match» := leading_parser:leadPrec "match " >> optional generalizingParam >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «match» := leading_parser:leadPrec "match " >> optional generalizingParam >> sepBy1 matchDiscr ", " >> optType >> " with " >> ppDedent matchAlts
@[builtinTermParser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
def funImplicitBinder := atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder