------------------------------------------------------------------------
-- The Agda standard library
--
-- Instances for the writer monad
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Effect.Monad.Writer.Instances where

open import Effect.Monad.Writer.Transformer

instance
  writerTFunctor = λ {s} {S} {f} {M} {{fun}} {{mo}} → functor {s} {S} {f} {M} {mo} fun
  writerTApplicative = λ {s} {S} {f} {M} {{mo}} {{mon}} → applicative {s} {S} {f} {M} {mo} mon
  writerTEmpty = λ {s} {S} {f} {M} {{e}} {{mo}} → empty {s} {S} {f} {M} {mo} e
  writerTChoice = λ {s} {S} {f} {M} {{ch}} {{mo}} → choice {s} {S} {f} {M} {mo} ch
  writerTApplicativeZero = λ {s} {S} {f} {M} {{mo}} {{mon}} → applicativeZero {s} {S} {f} {M} {mo} mon
  writerTAlternative = λ {s} {S} {f} {M} {{mo}} {{mpl}} → alternative {s} {S} {f} {M} {mo} mpl
  writerTMonad = λ {s} {S} {f} {M} {{mo}} {{mon}} → monad {s} {S} {f} {M} {mo} mon
  writerTMonadZero = λ {s} {S} {f} {M} {{mo}} {{mz}} → monadZero {s} {S} {f} {M} {mo} mz
  writerTMonadPlus = λ {s} {S} {f} {M} {{mo}} {{mpl}} → monadPlus {s} {S} {f} {M} {mo} mpl
  writerTMonadT = λ {s} {S} {f} {M} {{mo}} {{mon}} → monadT {s} {S} {f} {M} {mo} mon
  writerTMonadWriter = λ {s} {S} {f} {M} {{mo}} {{mon}} → monadWriter {s} {S} {f} {M} {mo} mon
  writerTLiftReaderT = λ {s} {S₁} {S₂} {f} {g} {M} {{fun}} {{mw}} → liftReaderT {s} {S₁} {S₂} {f} {g} {M} fun mw
  writerTLiftStateT = λ {s} {S₁} {S₂} {f} {g} {M} {{fun}} {{mw}} → liftStateT {s} {S₁} {S₂} {f} {g} {M} fun mw