perf: optimize unfolding constant lookup

leanprover · Nov 7, 2024 · 489c87a · 489c87a
1 parent c779f3a
commit 489c87a
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
@@ -831,10 +831,12 @@ mutual
           else
             unfoldDefault ()
     | .const declName lvls => do
+      let some cinfo ← getUnfoldableConstNoEx? declName | pure none
+      -- check smart unfolding only after `getUnfoldableConstNoEx?` because smart unfoldings have a
+      -- significant chance of not existing and `Environment.contains` misses are more costly
       if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
         return none
       else
-        let some cinfo ← getUnfoldableConstNoEx? declName | pure none
         unless cinfo.hasValue do return none
         deltaDefinition cinfo lvls
           (fun _ => pure none)