Lemmas about OptionT

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.

def OptionT.mapM' {m : Type u → Type v} {n : Type u → Type w} [Monad m] [AlternativeMonad n] [LawfulMonad n] [LawfulAlternative n] (f : m →ᵐ n) : OptionT m →ᵐ n

Bundled version of mapM. dtumad: we should probably just pick one of these (probably the hom class non-bundled approach)

@[simp]

theorem OptionT.mapM'_lift {α : Type u} {m : Type u → Type v} {n : Type u → Type w} [Monad m] [AlternativeMonad n] [LawfulMonad n] [LawfulAlternative n] (f : m →ᵐ n) (x : m α) : (fun {α : Type u} (x : OptionT m α) => (OptionT.mapM' f).toFun α x) (OptionT.lift x) = (fun {α : Type u} (x : m α) => f.toFun α x) x

@[simp]

theorem OptionT.mapM'_failure {α : Type u} {m : Type u → Type v} {n : Type u → Type w} [Monad m] [AlternativeMonad n] [LawfulMonad n] [LawfulAlternative n] (f : m →ᵐ n) : (fun {α : Type u} (x : OptionT m α) => (OptionT.mapM' f).toFun α x) failure = failure

@[simp]

theorem OptionT.mk_bind {α β : Type u} (m : Type u → Type v) [Monad m] [LawfulMonad m] (mx : m α) (my : α → m (Option β)) : OptionT.mk (mx >>= my) = do let x ← liftM mx OptionT.mk (my x)

@[simp]

theorem OptionT.liftM_elimM {m : Type u_1 → Type u_2} [Monad m] {α β : Type u_1} (x : m (Option α)) (y : m β) (z : α → m β) {n : Type u_1 → Type u_3} [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] : liftM (Option.elimM x y z) = Option.elimM (liftM x) (liftM y) fun (x : α) => liftM (z x)