From 3e65f586cc8b9be4c294eba67efa4a9ed708b787 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Feb 2021 15:39:07 -0800
Subject: [PATCH] fix: smart unfolding

---
 src/Lean/Meta/WHNF.lean | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index a012efcdfc..fb39744996 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -19,8 +19,8 @@ namespace Lean.Meta
 
 def smartUnfoldingSuffix := "_sunfold"
 
-@[inline] def mkSmartUnfoldingNameFor (n : Name) : Name :=
-  Name.mkStr n smartUnfoldingSuffix
+@[inline] def mkSmartUnfoldingNameFor (declName : Name) : Name :=
+  Name.mkStr declName smartUnfoldingSuffix
 
 register_builtin_option smartUnfolding : Bool := {
   defValue := true
@@ -439,11 +439,14 @@ mutual
             | _ => unfoldDefault ()
           else
             unfoldDefault ()
-    | Expr.const name lvls _ => do
-      let (some (cinfo@(ConstantInfo.defnInfo _))) ← getConstNoEx? name | pure none
-      deltaDefinition cinfo lvls
-        (fun _ => pure none)
-        (fun e => pure (some e))
+    | Expr.const declName lvls _ => do
+      if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
+        return none
+      else
+        let (some (cinfo@(ConstantInfo.defnInfo _))) ← getConstNoEx? declName | pure none
+        deltaDefinition cinfo lvls
+          (fun _ => pure none)
+          (fun e => pure (some e))
     | _ => return none
 end