Reverse of MonadExcept.ofExcept

Stream: lean4

[Adam Topaz]

MonadExcept.ofExcept converts e : ExceptT E m X to m X given MonadExcept E m. For some reason I need the reverse of this:

def foo [Monad m] [MonadExcept ε m] (e : m α) : ExceptT ε m α := .mk do
  try let a ← e ; return .ok a
  catch e => return .error e

Do we have such a function somewhere? I couldn't find it.

[Markus Himmel]

Not 100% sure, but possibly docs#observing

[Adam Topaz]

I guess it's docs#ExceptT.mk composed with that, yes.