From 2fee8059b6dd29ca121694f2a75453de567bb39a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Feb 2020 13:09:40 -0800
Subject: [PATCH] feat: add `induction` tactic parser

---
 lean4-mode/lean4-syntax.el       | 2 +-
 src/Init/Lean/Parser/Tactic.lean | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el
index 79617c5199..eb46a520af 100644
--- a/lean4-mode/lean4-syntax.el
+++ b/lean4-mode/lean4-syntax.el
@@ -17,7 +17,7 @@
     "match_syntax" "match" "nomatch" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
     "end" "this" "using" "using_well_founded" "namespace" "section"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
-    "attributes" "raw" "replacing"
+    "attributes" "raw" "replacing" "generalizing"
     "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
     "exists" "if" "then" "else" "assume" "from" "init_quot"
     "mutual" "def" "run_cmd")
diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index 7fa29ef081..d6ce54e95d 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/src/Init/Lean/Parser/Tactic.lean
@@ -36,7 +36,13 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «allGoals»   := parser! nonReservedSymbol "allGoals " >> tacticParser
 @[builtinTacticParser] def «skip»       := parser! nonReservedSymbol "skip"
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
-
+def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
+def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident >> many ident >> darrow >> termParser
+def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
+def withAlts : Parser := optional (" with " >> inductionAlts)
+def usingRec : Parser := optional (" using " >> ident)
+def generalizingVars := optional (" generalizing " >> many1 ident)
+@[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
 @[builtinTacticParser] def paren        := parser! "(" >> nonEmptySeq >> ")"
 @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
 @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"