Lemmas about OptionT

@[simp]

theorem OptionT.run_lift {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) : (OptionT.lift x).run = do let a ← x pure (some a)

theorem OptionT.monad_pure_eq_pure {m : Type u → Type v} {α : Type u} [Monad m] (x : α) : pure x = OptionT.pure x

theorem OptionT.monad_bind_eq_bind {m : Type u → Type v} {α β : Type u} [Monad m] (x : OptionT m α) (y : α → OptionT m β) : x >>= y = x.bind y

theorem OptionT.liftM_def {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) : liftM x = OptionT.lift x

def OptionT.mapM {m : Type u → Type v} {n : Type u → Type w} [AlternativeMonad n] (f : {α : Type u} → m α → n α) {α : Type u} (x : OptionT m α) : n α

Canonical lifting of a map from m α → n α to one from OptionT m α → n α given an Alternative n instance to handle failure.

Equations

• OptionT.mapM f x = do let __do_lift ← f x.run __do_lift.getM