perf: inline checkInterrupted

Amazingly, the extra result allocation seems to have triggered a mathlib heartbeat timeout
leanprover · Oct 13, 2023 · 6494af4 · 6494af4
1 parent 5aae741
commit 6494af4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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"