------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4