From 0fcf6217eca6f2fa1730d2e49008a608038b02c7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Nov 2020 06:43:14 -0800
Subject: [PATCH] feat: optional `:=` before constructors in the `inductive`
 command

@Kha In the documentation, I will always use `:=`. The idea is to
avoid the issue: why does `structure` have a `:=` but `inductive`
doesn't.
---
 src/Lean/Elab/Declaration.lean | 16 +++++++---------
 src/Lean/Parser/Command.lean   |  4 ++--
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 523bbc9db5..261cab3a2e 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -86,17 +86,15 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
 /-
-parser! "inductive " >> declId >> optDeclSig >> many ctor
-parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
-
-Remark: numTokens == 1 for regular `inductive` and 2 for `class inductive`.
+parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
+parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor
 -/
-private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTokens := 1) : CommandElabM InductiveView := do
+private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
   checkValidInductiveModifier modifiers
-  let (binders, type?) := expandOptDeclSig decl[numTokens + 1]
-  let declId           := decl[numTokens]
+  let (binders, type?) := expandOptDeclSig decl[2]
+  let declId           := decl[1]
   let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
-  let ctors      ← decl[numTokens + 2].getArgs.mapM fun ctor => withRef ctor do
+  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
     -- def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
     let ctorModifiers ← elabModifiers ctor[1]
     if ctorModifiers.isPrivate && modifiers.isPrivate then
@@ -122,7 +120,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTo
   }
 
 private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
-  inductiveSyntaxToView modifiers decl 2
+  inductiveSyntaxToView modifiers decl
 
 def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let v ← inductiveSyntaxToView modifiers stx
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index ebe69761d3..99fede8fa3 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -47,8 +47,8 @@ def «axiom»          := parser! "axiom " >> declId >> declSig
 def «example»        := parser! "example " >> declSig >> declVal
 def inferMod         := parser! atomic ("{" >> "}")
 def ctor             := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
-def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> many ctor
-def classInductive   := parser! atomic ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
+def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
+def classInductive   := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor
 def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
 def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
 def structInstBinder     := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"