Option Flatten?

Stream: lean4

[Mac]

Is there code in stdlib for some kind of Option.flatten that compresses an Option stack? For example:

def flatten : Option (Option a) -> Option a
| some v => v
| none => none

This comes up a lot in nested optionals within macros.

[Johan Commelin]

Does Lean 4 know that Option is a monad? Because this is the join.

[Mac]

No, in fact, Option is specifically not a Monad (OptionM is the monad version).