Equivalent to Haskell's hoistMaybe

Stream: Is there code for X?

[Chris Henson]

Does this definition:

def hoistOption [Monad m] : Option T → OptionT m T := OptionT.mk ∘ pure

exist somewhere already, or is there a more idiomatic way to write this in Lean?

[Eric Wieser]

I asked about this before here

[Chris Henson]

Eric Wieser said:

I asked about this before here

That's helpful, thanks! I tend to agree with you that it is nice to lift so long as it doesn't create any typeclass inefficiency problems.