@[inline]
def
StateT.run
{σ : Type u}
{m : Type u → Type v}
{α : Type u}
(x : StateT σ m α)
(s : σ)
:
m (α × σ)
Equations
- StateT.run x s = x s
@[inline]
def
StateT.run'
{σ : Type u}
{m : Type u → Type v}
[inst : Functor m]
{α : Type u}
(x : StateT σ m α)
(s : σ)
:
m α
Equations
- StateT.run' x s = (fun a => a.fst) <$> x s
noncomputable instance
instSubsingletonStateM
{σ : Type u_1}
{α : Type u_1}
[inst : Subsingleton σ]
[inst : Subsingleton α]
:
Subsingleton (StateM σ α)
@[inline]
def
StateT.pure
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
(a : α)
:
StateT σ m α
Equations
- StateT.pure a s = pure (a, s)
@[inline]
def
StateT.bind
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
{β : Type u}
(x : StateT σ m α)
(f : α → StateT σ m β)
:
StateT σ m β
Equations
- StateT.bind x f s = do let discr ← x s let x : α × σ := discr match x with | (a, s) => f a s
@[inline]
def
StateT.map
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
{β : Type u}
(f : α → β)
(x : StateT σ m α)
:
StateT σ m β
Equations
- StateT.map f x s = do let discr ← x s let x : α × σ := discr match x with | (a, s) => pure (f a, s)
@[inline]
def
StateT.orElse
{σ : Type u}
{m : Type u → Type v}
[inst : Alternative m]
{α : Type u}
(x₁ : StateT σ m α)
(x₂ : Unit → StateT σ m α)
:
StateT σ m α
Equations
- StateT.orElse x₁ x₂ s = HOrElse.hOrElse (x₁ s) fun x => x₂ () s
@[inline]
def
StateT.failure
{σ : Type u}
{m : Type u → Type v}
[inst : Alternative m]
{α : Type u}
:
StateT σ m α
Equations
- StateT.failure s = failure
instance
StateT.instAlternativeStateT
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
[inst : Alternative m]
:
Alternative (StateT σ m)
Equations
- StateT.instAlternativeStateT = Alternative.mk (fun {α} => StateT.failure) fun {α} => StateT.orElse
@[inline]
Equations
- StateT.get s = pure (s, s)
@[inline]
Equations
- StateT.set s' s = pure (PUnit.unit, s')
@[inline]
def
StateT.modifyGet
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
(f : σ → α × σ)
:
StateT σ m α
Equations
- StateT.modifyGet f s = pure (f s)
@[inline]
def
StateT.lift
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
(t : m α)
:
StateT σ m α
Equations
- StateT.lift t s = do let a ← t pure (a, s)
instance
StateT.instMonadFunctorStateT
(σ : Type u_1)
(m : Type u_1 → Type u_2)
[inst : Monad m]
:
MonadFunctor m (StateT σ m)
Equations
- StateT.instMonadFunctorStateT σ m = { monadMap := fun {α} f x s => f (α × σ) (x s) }
instance
StateT.instMonadExceptOfStateT
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
(ε : Type u_1)
[inst : MonadExceptOf ε m]
:
MonadExceptOf ε (StateT σ m)
Equations
- StateT.instMonadExceptOfStateT ε = { throw := fun {α} => StateT.lift ∘ throwThe ε, tryCatch := fun {α} x c s => tryCatchThe ε (x s) fun e => c e s }
instance
instMonadStateOfStateT
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
:
MonadStateOf σ (StateT σ m)
Equations
- instMonadStateOfStateT = { get := StateT.get, set := StateT.set, modifyGet := fun {α} => StateT.modifyGet }
instance
StateT.monadControl
(σ : Type u)
(m : Type u → Type v)
[inst : Monad m]
:
MonadControl m (StateT σ m)
Equations
- StateT.monadControl σ m = { stM := fun α => α × σ, liftWith := fun {α} f => do let s ← get liftM (f fun {β} x => StateT.run x s), restoreM := fun {α} x => do let discr ← liftM x let x : (fun α => α × σ) α := discr match x with | (a, s) => do set s pure a }
instance
StateT.tryFinally
{m : Type u → Type v}
{σ : Type u}
[inst : MonadFinally m]
[inst : Monad m]
:
MonadFinally (StateT σ m)