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)