From 6494af4513da28b13f3e3175e4cf59e24ad05dc8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 12 Oct 2023 14:05:00 +0200
Subject: [PATCH] perf: inline `checkInterrupted`

Amazingly, the extra result allocation seems to have triggered a mathlib
heartbeat timeout
---
 src/Lean/CoreM.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 2b87d66d8ec1..ce19929d3a4e 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -199,7 +199,7 @@ instance [MetaEval α] : MetaEval (CoreM α) where
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 
-def checkInterrupted : CoreM Unit := do
+@[inline] def checkInterrupted : CoreM Unit := do
   if (← IO.checkCanceled) then
     -- should never be visible to users!
     throw <| Exception.error .missing "elaboration interrupted"