Control.Eff.State

Definitions

data StateL : k -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Get : StateL lbl s s

Put : s -> StateL lbl s ()

State : Type -> Type -> Type

Totality: total
Visibility: public export

getAt : (0 lbl : k) -> Has (StateL lbl s) fs => Eff fs s

Totality: total
Visibility: export

get : Has (State s) fs => Eff fs s

Totality: total
Visibility: export

putAt : (0 lbl : k) -> Has (StateL lbl s) fs => s -> Eff fs ()

Totality: total
Visibility: export

put : Has (State s) fs => s -> Eff fs ()

Totality: total
Visibility: export

modifyAt : (0 lbl : k) -> Has (StateL lbl s) fs => (s -> s) -> Eff fs ()

Totality: total
Visibility: export

modify : Has (State s) fs => (s -> s) -> Eff fs ()

Totality: total
Visibility: export

handleState : {0 m : Type -> Type} -> m s -> (s -> m ()) -> StateL lbl s a -> m a

Totality: total
Visibility: export

runStateAt : (0 lbl : k) -> {auto {conArg:2235} : Has (StateL lbl s) fs} -> s -> Eff fs t -> Eff (fs - StateL lbl s) (t, s)

Totality: total
Visibility: export

runState : {auto {conArg:2355} : Has (State s) fs} -> s -> Eff fs t -> Eff (fs - State s) (t, s)

Totality: total
Visibility: export