Lean4
/-- Creates an instance of `Monad`, with explicitly given `empty` and `append` operations.
Previously, this would have used an instance of `[Monoid ω]` as input.
In practice, however, `WriterT` is used for logging and creating lists so restricting to
monoids with `Mul` and `One` can make `WriterT` cumbersome to use.
This is used to derive instances for both `[EmptyCollection ω] [Append ω]` and `[Monoid ω]`.
-/
@[reducible, inline]
def monad (empty : ω) (append : ω → ω → ω) : Monad (WriterT ω M)
where
map := fun f (cmd : M _) ↦ WriterT.mk <| (fun (a, w) ↦ (f a, w)) <$> cmd
pure := fun a ↦ pure (f := M) (a, empty)
bind := fun (cmd : M _) f ↦ WriterT.mk <| cmd >>= fun (a, w₁) ↦ (fun (b, w₂) ↦ (b, append w₁ w₂)) <$> (f a)
