fix: sharing bug

digama0 · Oct 30, 2023 · 2d54c3d · 2d54c3d
1 parent 68da6f1
commit 2d54c3d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Lean4Lean/TypeChecker.lean b/Lean4Lean/TypeChecker.lean
@@ -319,7 +319,7 @@ def whnfCore' (e : Expr) (cheapRec := false) (cheapProj := false) : RecM Expr :=
   | .app .. | .letE .. | .proj .. => pure ()
   if let some r := (← get).whnfCoreCache.find? e then
     return r
-  let save r := do
+  let rec save r := do
     if !cheapRec && !cheapProj then
       modify fun s => { s with whnfCoreCache := s.whnfCoreCache.insert e r }
     return r