Lemmas About Option Monad Transformer

This file contains lemmas about the behavior of OptionT and OptionT.run.

@[simp]

theorem OptionT.run_monadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [Monad m] [LawfulMonad m] [MonadLiftT n m] (x : n α) : (monadLift x).run = some <$> monadLift x

@[simp]

theorem OptionT.run_mapConst {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : β) : (Functor.mapConst y x).run = Option.map (Function.const α y) <$> x.run

@[simp]

theorem OptionT.run_monadMap {m : Type u_1 → Type u_2} {α : Type u_1} {x : OptionT m α} {n : Type u_1 → Type u_3} [MonadFunctorT n m] (f : {α : Type u_1} → n α → n α) : (monadMap f x).run = monadMap f x.run

instance OptionT.instLawfulMonadStateOfOfLawfulMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : LawfulMonadStateOf σ (OptionT m)