From a2e8a41f33f5fba43e9991c05ad15a6668d28948 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Sep 2020 17:38:51 -0700 Subject: [PATCH] feat: `rewrite` tactic parser --- src/Lean/Parser/Tactic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index a83b194efd..13b534c850 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -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