From cbb108e51f8a2925a5ef8ecfb2e6ffa47a4c203b Mon Sep 17 00:00:00 2001 From: Jannis Limperg Date: Fri, 22 Nov 2024 19:39:15 +0100 Subject: [PATCH] RPINF: disable cache --- Aesop/RPINF.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Aesop/RPINF.lean b/Aesop/RPINF.lean index 9bb665c..500f942 100644 --- 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