theorem
monadLift_map
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(f : α → β)
(ma : m α)
:
theorem
monadLift_seq
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(mf : m (α → β))
(ma : m α)
:
theorem
monadLift_seqLeft
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(x : m α)
(y : m β)
:
theorem
monadLift_seqRight
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(x : m α)
(y : m β)
:
We duplicate the theorems for monadLift
to liftM
since rw
matches on syntax only.
@[simp]
theorem
liftM_pure
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α : Type u}
(a : α)
:
@[simp]
theorem
liftM_map
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(f : α → β)
(ma : m α)
:
@[simp]
theorem
liftM_seq
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(mf : m (α → β))
(ma : m α)
:
@[simp]
theorem
liftM_seqLeft
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(x : m α)
(y : m β)
:
@[simp]
theorem
liftM_seqRight
{m : Type u → Type v}
{n : Type u → Type w}
[Monad m]
[Monad n]
[MonadLiftT m n]
[LawfulMonadLiftT m n]
{α β : Type u}
[LawfulMonad m]
[LawfulMonad n]
(x : m α)
(y : m β)
: