From 9d1dbada7949f1fdd6c4a6fd6311df2ea99ae8d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 12 Mar 2022 13:44:33 -0800
Subject: [PATCH] feat: only try to generate equation theorems for definitions
 whose types are not propositions

---
 src/Lean/Meta/Eqns.lean | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index 875bb7e00e..297d69f5df 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Basic
+import Lean.Meta.InferType
 
 namespace Lean.Meta
 
@@ -41,10 +42,17 @@ def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
     throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
   getEqnsFnsRef.modify (f :: ·)
 
+private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
+  if let some (.defnInfo info) := (← getEnv).find? declName then
+    return !(← isProp info.type)
+  else
+    return false
+
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  for f in (← getEqnsFnsRef.get) do
-    if let some r ← f declName then
-      return some r
+  if (← shouldGenerateEqnThms declName) then
+    for f in (← getEqnsFnsRef.get) do
+      if let some r ← f declName then
+        return some r
   return none
 
 def GetUnfoldEqnFn := Name → MetaM (Option Name)
@@ -82,9 +90,10 @@ def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   getUnfoldEqnFnsRef.modify (f :: ·)
 
 def getUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
-  for f in (← getUnfoldEqnFnsRef.get) do
-    if let some r ← f declName then
-      return some r
-  return none
+  if (← shouldGenerateEqnThms declName) then
+    for f in (← getUnfoldEqnFnsRef.get) do
+      if let some r ← f declName then
+        return some r
+   return none
 
 end Lean.Meta