Control.Monad.Indexed.State

Definitions

record IndexedStateT : Type -> (x : Type) -> (y : Type) -> (Type -> x -> y -> Type) -> Type -> x -> y -> Type

  Support for wrapping an IndexedMonad in another stateful
  Monad.
  The order of the parameters may seem odd compared to other
  StateT types, but the ordering is such that an IndexedMonad 
  type can be elevated to a TransitionIndexedMonad type without 
  much refactoring.

Totality: total
Visibility: public export
Constructor: 

ST : (stateType -> m (stateType, a) i j) -> IndexedStateT stateType x y m a i j

Projection: 

.runStateT' : IndexedStateT stateType x y m a i j -> stateType -> m (stateType, a) i j

Hints:

IndexedMonad z m => IndexedApplicative z (IndexedStateT stateType z z m)

IndexedFunctor x y f => IndexedFunctor x y (IndexedStateT stateType x y f)

IndexedMonad z m => IndexedMonad z (IndexedStateT stateType z z m)

.runStateT' : IndexedStateT stateType x y m a i j -> stateType -> m (stateType, a) i j

Visibility: public export

runStateT' : IndexedStateT stateType x y m a i j -> stateType -> m (stateType, a) i j

Visibility: public export

runStateT : stateType -> IndexedStateT stateType x y m a i j -> m (stateType, a) i j

Visibility: public export

evalStateT : IndexedFunctor x y m => stateType -> IndexedStateT stateType x y m a i j -> m a i j

Visibility: public export

execStateT : IndexedFunctor x y m => stateType -> IndexedStateT stateType x y m a i j -> m stateType i j

Visibility: public export

mapStateT : (m (s, a) i j -> n (s, b) i j) -> IndexedStateT s x y m a i j -> IndexedStateT s x y n b i j

Visibility: public export

lift : IndexedFunctor x y m => m a i j -> IndexedStateT stateType x y m a i j

Visibility: public export

get : IndexedApplicative z m => IndexedStateT stateType z z m stateType i i

Visibility: public export

gets : IndexedApplicative z m => (stateType -> a) -> IndexedStateT stateType z z m a i i

Visibility: public export

put : IndexedApplicative z m => stateType -> IndexedStateT stateType z z m () i i

Visibility: public export

modify : IndexedMonad z m => (stateType -> stateType) -> IndexedStateT stateType z z m () i i

Visibility: public export