Documentation

Init.Control.Lawful.MonadLift.Lemmas

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 α) :
monadLift (mf <*> ma) = monadLift mf <*> monadLift ma
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 β) :
monadLift (x <* y) = monadLift x <* monadLift y
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 β) :
monadLift (x *> y) = monadLift x *> monadLift y

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_bind {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α β : Type u} (ma : m α) (f : αm β) :
liftM (ma >>= f) = do let aliftM ma liftM (f 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 α) :
liftM (f <$> ma) = f <$> liftM ma
@[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 α) :
liftM (mf <*> ma) = liftM mf <*> liftM ma
@[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 β) :
liftM (x <* y) = liftM x <* liftM y
@[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 β) :
liftM (x *> y) = liftM x *> liftM y