Documentation

ToMathlib.Control.WriterT

Laws for well behaved monadic failure operation #

source
@[simp]
theorem WriterT.run_mk {m : Type u → Type v} [Monad m] {α ω : Type u} [LawfulMonad m] (x : m (α × ω)) :
(WriterT.mk x).run = x
source
@[simp]
theorem WriterT.run_tell {m : Type u → Type v} [Monad m] {ω : Type u} (w : ω) :
(tell w).run = pure (PUnit.unit, w)
source
@[simp]
theorem WriterT.run_monadLift {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) :
(monadLift x).run = (fun (x : α) => (x, 1)) <$> x
source
theorem WriterT.liftM_def {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) :
liftM x = WriterT.mk ((fun (x : α) => (x, 1)) <$> x)
source
theorem WriterT.monadLift_def {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) :
MonadLift.monadLift x = WriterT.mk ((fun (x : α) => (x, 1)) <$> x)
source
theorem WriterT.bind_def {m : Type u → Type v} [Monad m] {ω α β : Type u} [Monoid ω] (x : WriterT ω m α) (f : α → WriterT ω m β) :
x >>= f = WriterT.mk do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ * x) <$> f a
source
@[simp]
theorem WriterT.run_pure {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] [LawfulMonad m] (x : α) :
(pure x).run = pure (x, 1)
source
@[simp]
theorem WriterT.run_bind {m : Type u → Type v} [Monad m] {ω α β : Type u} [Monoid ω] [LawfulMonad m] (x : WriterT ω m α) (f : α → WriterT ω m β) :
(x >>= f).run = do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ * x) <$> (f a).run
source
@[simp]
theorem WriterT.run_seqLeft {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] {α β : Type u} (x : WriterT ω m α) (y : WriterT ω m β) :
(x *> y).run = do let z ← x.run (Prod.map id fun (x : ω) => z.snd * x) <$> y.run
source
@[simp]
theorem WriterT.run_map {m : Type u → Type v} [Monad m] {ω α β : Type u} [Monoid ω] (x : WriterT ω m α) (f : α → β) :
(f <$> x).run = Prod.map f id <$> x.run
source
@[inline]
def WriterT.orElse {m : Type u → Type v} [AlternativeMonad m] {ω α : Type u} (x₁ : WriterT ω m α) (x₂ : Unit → WriterT ω m α) :
WriterT ω m α
Equations
Instances For
    source
    @[inline]
    def WriterT.failure {m : Type u → Type v} [AlternativeMonad m] {ω α : Type u} :
    WriterT ω m α
    Equations
    Instances For
      source
      instance WriterT.instAlternativeMonadOfMonoid_toMathlib {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] :
      AlternativeMonad (WriterT ω m)
      Equations
      source
      @[simp]
      theorem WriterT.run_failure {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] {α : Type u} :
      failure.run = failure
      source
      instance WriterT.instLawfulAlternativeOfLawfulMonad_toMathlib {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] [LawfulMonad m] [LawfulAlternative m] :
      LawfulAlternative (WriterT ω m)
      source
      instance WriterT.instLawfulMonadLiftOfLawfulMonad_toMathlib {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] [LawfulMonad m] :
      LawfulMonadLift m (WriterT ω m)