Control.Eff.Writer

Definitions

data WriterL : k -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

Tell : w -> WriterL lbl w ()

Writer : Type -> Type -> Type

Totality: total
Visibility: public export

tellAt : (0 lbl : k) -> Has (WriterL lbl w) fs => w -> Eff fs ()

Totality: total
Visibility: export

tell : Has (Writer w) fs => w -> Eff fs ()

Totality: total
Visibility: export

handleWriter : {0 m : Type -> Type} -> (w -> m ()) -> WriterL lbl w a -> m a

Totality: total
Visibility: export

foldWriterAt : (0 lbl : k) -> {auto {conArg:2068} : Has (WriterL lbl w) fs} -> u -> (u -> w -> u) -> Eff fs t -> Eff (fs - WriterL lbl w) (t, u)

Totality: total
Visibility: export

foldWriter : {auto {conArg:2211} : Has (Writer w) fs} -> u -> (u -> w -> u) -> Eff fs t -> Eff (fs - Writer w) (t, u)

Totality: total
Visibility: export

runWriterAt : (0 lbl : k) -> {auto {conArg:2271} : Has (WriterL lbl w) fs} -> Monoid w => Eff fs t -> Eff (fs - WriterL lbl w) (t, w)

Totality: total
Visibility: export

runWriter : {auto {conArg:2332} : Has (Writer w) fs} -> Monoid w => Eff fs t -> Eff (fs - Writer w) (t, w)

Totality: total
Visibility: export