From 9f50f44eed0ea3b49490b77c303b7e4f6e54fc2a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 8 Oct 2023 17:22:14 -0700
Subject: [PATCH] perf: missing cache at `whnfImp`

---
 src/Lean/Meta/WHNF.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 4759521b74..94a3db21a5 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -871,8 +871,8 @@ partial def whnfImp (e : Expr) : MetaM Expr :=
         | some v => cache useCache e v
         | none   =>
           match (← unfoldDefinition? e') with
-          | some e => whnfImp e
-          | none   => cache useCache e e'
+          | some e'' => cache useCache e (← whnfImp e'')
+          | none => cache useCache e e'
 
 /-- If `e` is a projection function that satisfies `p`, then reduce it -/
 def reduceProjOf? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do