Equations
- StateRefT' ω σ m α = ReaderT (ST.Ref ω σ) m α
@[inline]
def
StateRefT'.run
{ω : Type}
{σ : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT (ST ω) m]
{α : Type}
(x : StateRefT' ω σ m α)
(s : σ)
:
m (α × σ)
Equations
- StateRefT'.run x s = do let ref ← ST.mkRef s let a ← x ref let s ← ST.Ref.get ref pure (a, s)
@[inline]
def
StateRefT'.run'
{ω : Type}
{σ : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT (ST ω) m]
{α : Type}
(x : StateRefT' ω σ m α)
(s : σ)
:
m α
Equations
- StateRefT'.run' x s = do let discr ← StateRefT'.run x s match discr with | (a, snd) => pure a
@[inline]
def
StateRefT'.lift
{ω : Type}
{σ : Type}
{m : Type → Type}
{α : Type}
(x : m α)
:
StateRefT' ω σ m α
Equations
- StateRefT'.lift x x = x
instance
StateRefT'.instMonadStateRefT'
{ω : Type}
{σ : Type}
{m : Type → Type}
[inst : Monad m]
:
Monad (StateRefT' ω σ m)
Equations
- StateRefT'.instMonadStateRefT' = inferInstanceAs (Monad (ReaderT (ST.Ref ω σ) fun α => m α))
instance
StateRefT'.instMonadLiftStateRefT'
{ω : Type}
{σ : Type}
{m : Type → Type}
:
MonadLift m (StateRefT' ω σ m)
Equations
- StateRefT'.instMonadLiftStateRefT' = { monadLift := fun {α} => StateRefT'.lift }
instance
StateRefT'.instMonadFunctorStateRefT'
{ω : Type}
(σ : Type)
(m : Type → Type)
[inst : Monad m]
:
MonadFunctor m (StateRefT' ω σ m)
Equations
- StateRefT'.instMonadFunctorStateRefT' σ m = inferInstanceAs (MonadFunctor m (ReaderT (ST.Ref ω σ) fun α => m α))
instance
StateRefT'.instAlternativeStateRefT'
{ω : Type}
{σ : Type}
{m : Type → Type}
[inst : Alternative m]
[inst : Monad m]
:
Alternative (StateRefT' ω σ m)
Equations
- StateRefT'.instAlternativeStateRefT' = inferInstanceAs (Alternative (ReaderT (ST.Ref ω σ) fun α => m α))
@[inline]
def
StateRefT'.get
{ω : Type}
{σ : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT (ST ω) m]
:
StateRefT' ω σ m σ
Equations
- StateRefT'.get ref = ST.Ref.get ref
@[inline]
def
StateRefT'.set
{ω : Type}
{σ : Type}
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT (ST ω) m]
(s : σ)
:
StateRefT' ω σ m PUnit
Equations
- StateRefT'.set s ref = ST.Ref.set ref s
@[inline]
def
StateRefT'.modifyGet
{ω : Type}
{σ : Type}
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : MonadLiftT (ST ω) m]
(f : σ → α × σ)
:
StateRefT' ω σ m α
Equations
- StateRefT'.modifyGet f ref = ST.Ref.modifyGet ref f
instance
StateRefT'.instMonadStateOfStateRefT'
{ω : Type}
{σ : Type}
{m : Type → Type}
[inst : MonadLiftT (ST ω) m]
[inst : Monad m]
:
MonadStateOf σ (StateRefT' ω σ m)
Equations
- StateRefT'.instMonadStateOfStateRefT' = { get := StateRefT'.get, set := StateRefT'.set, modifyGet := fun {α} => StateRefT'.modifyGet }
instance
StateRefT'.instMonadExceptOfStateRefT'
{ω : Type}
{σ : Type}
{m : Type → Type}
(ε : Type u_1)
[inst : MonadExceptOf ε m]
:
MonadExceptOf ε (StateRefT' ω σ m)
Equations
- StateRefT'.instMonadExceptOfStateRefT' ε = { throw := fun {α} => StateRefT'.lift ∘ throwThe ε, tryCatch := fun {α} x c s => tryCatchThe ε (x s) fun e => c e s }
instance
instMonadControlStateRefT'
(ω : Type)
(σ : Type)
(m : Type → Type)
:
MonadControl m (StateRefT' ω σ m)
Equations
- instMonadControlStateRefT' ω σ m = inferInstanceAs (MonadControl m (ReaderT (ST.Ref ω σ) fun α => m α))
instance
instMonadFinallyStateRefT'
{m : Type → Type}
{ω : Type}
{σ : Type}
[inst : MonadFinally m]
[inst : Monad m]
:
MonadFinally (StateRefT' ω σ m)
Equations
- instMonadFinallyStateRefT' = inferInstanceAs (MonadFinally (ReaderT (ST.Ref ω σ) fun α => m α))