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

chore: rwRuleSeq ; => ,

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-17 07:05:38 -07:00
parent 26ed304071
commit 9d1f2b644f
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/Tactic.lean
View file

@ -56,7 +56,7 @@ def location := parser! "at " >> (locationWildcard <|> locationTarget <|
@[builtinTacticParser] def changeWith := parser! nonReservedSymbol "change " >> termParser >> " with " >> termParser >> optional location
def rwRule := parser! optional (unicodeSymbol "←" "<-") >> termParser
def rwRuleSeq := parser! "[" >> sepBy1 rwRule "; " true >> "]"
def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
@[builtinTacticParser] def «rewrite» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRule >> optional location
@[builtinTacticParser] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location