Monad combinators, as in Haskell's Control.Monad.

def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α

Collapses two layers of monadic structure into one, passing the effects of the inner monad through the outer.

def condM {m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α

Executes tm or fm depending on whether the result of mbool is true or false respectively.