Skip to content

Commit 4311237

Browse files
authored
chore: add CoreM.toIO' (#11325)
This PR adds `CoreM.toIO'`, the analogue of `CoreM.toIO` dropping the state from the return type, and similarly for `TermElabM.toIO'` and `MetaM.toIO'`.
1 parent 4135674 commit 4311237

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/Lean/CoreM.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -435,6 +435,9 @@ def mkFreshUserName (n : Name) : CoreM Name :=
435435
| Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx
436436
| Except.ok a => return a
437437

438+
@[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
439+
(·.1) <$> x.toIO ctx s
440+
438441
-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
439442
protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
440443
controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)

0 commit comments

Comments
 (0)