RPINF: disable cache

leanprover-community · Nov 22, 2024 · cbb108e · cbb108e
1 parent 0b6bcc2
commit cbb108e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Aesop/RPINF.lean b/Aesop/RPINF.lean
@@ -136,7 +136,7 @@ variable [Monad m] [MonadRPINF m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
 @[specialize]
 partial def pinfCore (statsRef : IO.Ref PINFStats) (e : Expr) (type? : Option Expr) : m Expr :=
   withIncRecDepth do
-  checkCache e λ _ => do
+  -- checkCache e λ _ => do
     let (e, ti) ← time $ whnf e
     statsRef.modify λ s => { s with whnf := s.whnf + ti }
     match e with