def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type

Equations

• StateRefT' ω σ m α = ReaderT (ST.Ref ω σ) m α

Recall that StateRefT is a macro that infers ω from the m.

@[inline]

def StateRefT'.run {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [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} [Monad m] [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} [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) [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} [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m)

Equations

• StateRefT'.instAlternativeStateRefT' = inferInstanceAs (Alternative (ReaderT (ST.Ref ω σ) fun α => m α))

@[inline]

def StateRefT'.get {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ

Equations

• StateRefT'.get ref = ST.Ref.get ref

@[inline]

def StateRefT'.set {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [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} [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α

Equations

• StateRefT'.modifyGet f ref = ST.Ref.modifyGet ref f

instance StateRefT'.instMonadStateOfStateRefT' {ω : Type} {σ : Type} {m : Type → Type} [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m)

Equations

• StateRefT'.instMonadStateOfStateRefT' = { get := StateRefT'.get, set := StateRefT'.set, modifyGet := fun {α} => StateRefT'.modifyGet }

@[always_inline]

instance StateRefT'.instMonadExceptOfStateRefT' {ω : Type} {σ : Type} {m : Type → Type} (ε : Type u_1) [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} [MonadFinally m] [Monad m] : MonadFinally (StateRefT' ω σ m)

Equations

• instMonadFinallyStateRefT' = inferInstanceAs (MonadFinally (ReaderT (ST.Ref ω σ) fun α => m α))