instance instLawfulMonadLiftTOfLawfulMonadLift (m : Type u → Type v) (n : Type u → Type w) (o : Type u → Type x) [Monad m] [Monad n] [Monad o] [MonadLift n o] [MonadLiftT m n] [LawfulMonadLift n o] [LawfulMonadLiftT m n] : LawfulMonadLiftT m o

instance instLawfulMonadLiftT (m : Type u → Type v) [Monad m] : LawfulMonadLiftT m m

instance StateT.instLawfulMonadLift {m : Type u → Type v} [Monad m] [LawfulMonad m] {σ : Type u} : LawfulMonadLift m (StateT σ m)

instance ReaderT.instLawfulMonadLift {m : Type u → Type v} [Monad m] {ρ : Type u} : LawfulMonadLift m (ReaderT ρ m)

@[simp]

theorem OptionT.lift_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u} (a : α) : OptionT.lift (pure a) = pure a

@[simp]

theorem OptionT.lift_bind {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (ma : m α) (f : α → m β) : OptionT.lift (ma >>= f) = do let a ← OptionT.lift ma OptionT.lift (f a)

instance OptionT.instLawfulMonadLift {m : Type u → Type v} [Monad m] [LawfulMonad m] : LawfulMonadLift m (OptionT m)

@[simp]

theorem ExceptT.lift_bind {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β ε : Type u} (ma : m α) (f : α → m β) : ExceptT.lift (ma >>= f) = do let a ← ExceptT.lift ma ExceptT.lift (f a)

instance ExceptT.instLawfulMonadLift {m : Type u → Type v} [Monad m] [LawfulMonad m] {ε : Type u} : LawfulMonadLift m (ExceptT ε m)

instance ExceptT.instLawfulMonadLiftExcept {m : Type u → Type v} [Monad m] [LawfulMonad m] {ε : Type u} : LawfulMonadLift (Except ε) (ExceptT ε m)

instance StateRefT'.instLawfulMonadLift {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m)

instance StateCpsT.instLawfulMonadLiftOfLawfulMonad {m : Type u → Type v} {σ : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (StateCpsT σ m)

instance ExceptCpsT.instLawfulMonadLiftOfLawfulMonad {m : Type u → Type v} {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT ε m)