diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 89532d9c14..81ec44a9ad 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -142,6 +142,7 @@ def getSimpLetCase (n : Name) (t : Expr) (v : Expr) (b : Expr) : MetaM SimpLetCa return SimpLetCase.dep partial def simp (e : Expr) : M Result := withIncRecDepth do + checkMaxHeartbeats "simp" let cfg ← getConfig if (← isProof e) then return { expr := e }