From 2ea4d016c40d03e39ef65162ed73c9589b249db6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 11 Mar 2026 06:34:11 +0900 Subject: [PATCH] doc: remark that CoreM.toIO ignores ctx.initHeartbeats (#12859) This is slightly surprising behavior, and so should be in the docstring. --- src/Lean/CoreM.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 6732c5e2ff..87d4e59d63 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -431,6 +431,10 @@ def mkFreshUserName (n : Name) : CoreM Name := @[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α := Prod.fst <$> x.run ctx s +/-- +Run a `CoreM` monad in IO. +Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.getNumHeartbeats`. +-/ @[inline] def CoreM.toIO (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do match (← (x.run { ctx with initHeartbeats := (← IO.getNumHeartbeats) } s).toIO') with | Except.error (Exception.error _ msg) => throw <| IO.userError (← msg.toString) @@ -440,7 +444,7 @@ def mkFreshUserName (n : Name) : CoreM Name := @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α := (·.1) <$> x.toIO ctx s --- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]` +/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α := controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)