From 05147fd3520adb35aa1d0df86bb2273373e4b5e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 May 2021 17:37:41 -0700
Subject: [PATCH] fix: do not generate injectivity theorems for unsafe
 inductive datatypes

---
 src/Lean/Meta/Injective.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index 6db33966bd..f21db51b61 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -140,10 +140,11 @@ register_builtin_option genInjective : Bool := {
 def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
   if (← getEnv).contains ``Eq.propIntro && genInjective.get (← getOptions) &&  !(← isInductivePredicate declName) then
     let info ← getConstInfoInduct declName
-    for ctor in info.ctors do
-      let ctorVal ← getConstInfoCtor ctor
-      if ctorVal.numFields > 0 then
-        mkInjectiveTheorem ctorVal
-        mkInjectiveEqTheorem ctorVal
+    unless info.isUnsafe do
+      for ctor in info.ctors do
+        let ctorVal ← getConstInfoCtor ctor
+        if ctorVal.numFields > 0 then
+          mkInjectiveTheorem ctorVal
+          mkInjectiveEqTheorem ctorVal
 
 end Lean.Meta