From bf583f606533ed2bd97e485d9c5dfda9e58dc651 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 May 2021 22:36:45 -0700
Subject: [PATCH] chore: add placeholders for `mkInjectiveTheorems`

We can activate them yet since the method is failing when there are
heterogeous equalities in the injectivity theorem type.
---
 src/Lean/Elab/Inductive.lean | 3 +++
 src/Lean/Elab/Structure.lean | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index ecda085489..685fc63c01 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -9,6 +9,7 @@ import Lean.Util.CollectLevelParams
 import Lean.Util.Constructions
 import Lean.Meta.CollectFVars
 import Lean.Meta.SizeOf
+import Lean.Meta.Injective
 import Lean.Meta.IndPredBelow
 import Lean.Elab.Command
 import Lean.Elab.DefView
@@ -519,6 +520,8 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
     mkInductiveDecl vars views
     mkSizeOfInstances view0.declName
     Lean.Meta.IndPredBelow.mkBelow view0.declName
+    -- for view in views do
+    --  mkInjectiveTheorems view.declName
   applyDerivingHandlers views
 
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 6cf47c33aa..a954c987c2 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Parser.Command
 import Lean.Meta.Closure
 import Lean.Meta.SizeOf
+import Lean.Meta.Injective
 import Lean.Elab.Command
 import Lean.Elab.DeclModifiers
 import Lean.Elab.DeclUtil
@@ -581,6 +582,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
             }
             unless isClass do
               mkSizeOfInstances declName
+              -- mkInjectiveTheorems declName
             return declName
   derivingClassViews.forM fun view => view.applyHandlers #[declName]