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

feat: rewrite tactic parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-16 17:38:51 -07:00
parent c620a2a59d
commit a2e8a41f33
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -55,6 +55,11 @@ def location := parser! "at " >> (locationWildcard <|> locationTarget <|
@[builtinTacticParser] def change := parser! nonReservedSymbol "change " >> termParser >> optional location
@[builtinTacticParser] def changeWith := parser! nonReservedSymbol "change " >> termParser >> " with " >> termParser >> optional location
def rwRule := parser! optional (unicodeSymbol "←" "<-") >> termParser
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
def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
def altRHS := Term.hole <|> Term.syntheticHole <|> indentedNonEmptySeq
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS