From 2bf10b3d2c75b8a693469e858d2582d016df6402 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jul 2020 15:05:16 -0700
Subject: [PATCH] feat: add `inferMod` field to `CtorView`

---
 src/Lean/Elab/Declaration.lean | 3 ++-
 src/Lean/Elab/Inductive.lean   | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 253048c8c1..53807622b6 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -159,8 +159,9 @@ withDeclId declId fun name => do
     let ctorName := ctor.getIdAt 2;
     let ctorName := declName ++ ctorName;
     ctorName ← applyVisibility (ctor.getArg 2) ctorModifiers.visibility ctorName;
+    let inferMod := !(ctor.getArg 3).isNone;
     let (binders, type?) := expandOptDeclSig (ctor.getArg 4);
-    pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+    pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
   };
   pure {
     ref           := decl,
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 5f5e54003a..0430659ff8 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -13,12 +13,13 @@ namespace Command
 structure CtorView :=
 (ref       : Syntax)
 (modifiers : Modifiers)
+(inferMod  : Bool)  -- true if `{}` is used in the constructor declaration
 (declName  : Name)
 (binders   : Syntax)
 (type?     : Option Syntax)
 
 instance CtorView.inhabited : Inhabited CtorView :=
-⟨{ ref := arbitrary _, modifiers := {}, declName := arbitrary _, binders := arbitrary _, type? := none }⟩
+⟨{ ref := arbitrary _, modifiers := {}, inferMod := false, declName := arbitrary _, binders := arbitrary _, type? := none }⟩
 
 structure InductiveView :=
 (ref           : Syntax)