instance
instSubsingletonStateM
{σ α : Type u_1}
[Subsingleton σ]
[Subsingleton α]
:
Subsingleton (StateM σ α)
@[inline]
Fails with a recoverable error. The state is rolled back on error recovery.
Equations
Instances For
instance
StateT.instAlternative
{σ : Type u}
{m : Type u → Type v}
[Monad m]
[Alternative m]
:
Alternative (StateT σ m)
Equations
@[inline]
def
StateT.modifyGet
{σ : Type u}
{m : Type u → Type v}
[Monad m]
{α : Type u}
(f : σ → α × σ)
:
StateT σ m α
Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.
It is equivalent to do let (a, s) := f (← StateT.get); StateT.set s; pure a
. However, using
StateT.modifyGet
may lead to better performance because it doesn't add a new reference to the
state value, and additional references can inhibit in-place updates of data.
Equations
Instances For
@[inline]
Runs an action from the underlying monad in the monad with state. The state is not modified.
This function is typically implicitly accessed via a MonadLiftT
instance as part of automatic
lifting.
Equations
Instances For
@[always_inline]
instance
StateT.instMonadFunctor
(σ : Type u_1)
(m : Type u_1 → Type u_2)
:
MonadFunctor m (StateT σ m)
Equations
@[always_inline]
instance
StateT.instMonadExceptOf
{σ : Type u}
{m : Type u → Type v}
[Monad m]
(ε : Type u_1)
[MonadExceptOf ε m]
:
MonadExceptOf ε (StateT σ m)
Equations
instance
instMonadStateOfStateTOfMonad
{σ : Type u}
{m : Type u → Type v}
[Monad m]
:
MonadStateOf σ (StateT σ m)
Equations
@[always_inline]
instance
StateT.monadControl
(σ : Type u)
(m : Type u → Type v)
[Monad m]
:
MonadControl m (StateT σ m)
Equations
@[always_inline]
instance
StateT.tryFinally
{m : Type u → Type v}
{σ : Type u}
[MonadFinally m]
[Monad m]
:
MonadFinally (StateT σ m)