Documentation

Init.Control.State

def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) :
Type (maxuv)
Equations
@[inline]
def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) :
m (α × σ)
Equations
@[inline]
def StateT.run' {σ : Type u} {m : Type u → Type v} [inst : Functor m] {α : Type u} (x : StateT σ m α) (s : σ) :
m α
Equations
def StateM (σ : Type u) (α : Type u) :
Equations
@[inline]
def StateT.pure {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α) :
StateT σ m α
Equations
@[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 match __discr 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 match __discr with | (a, s) => pure (f a, s)
@[always_inline]
instance StateT.instMonadStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] :
Monad (StateT σ m)
Equations
  • StateT.instMonadStateT = Monad.mk
@[inline]
def StateT.orElse {σ : Type u} {m : Type u → Type v} [inst : Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : UnitStateT σ m α) :
StateT σ m α
Equations
@[inline]
def StateT.failure {σ : Type u} {m : Type u → Type v} [inst : Alternative m] {α : Type u} :
StateT σ m α
Equations
instance StateT.instAlternativeStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] [inst : Alternative m] :
Equations
  • StateT.instAlternativeStateT = Alternative.mk (fun {α} => StateT.failure) fun {α} => StateT.orElse
@[inline]
def StateT.get {σ : Type u} {m : Type u → Type v} [inst : Monad m] :
StateT σ m σ
Equations
@[inline]
def StateT.set {σ : Type u} {m : Type u → Type v} [inst : Monad m] :
σStateT σ m PUnit
Equations
@[inline]
def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (f : σα × σ) :
StateT σ m α
Equations
@[inline]
def StateT.lift {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (t : m α) :
StateT σ m α
Equations
instance StateT.instMonadLiftStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] :
MonadLift m (StateT σ m)
Equations
  • StateT.instMonadLiftStateT = { monadLift := fun {α} => StateT.lift }
@[always_inline]
instance StateT.instMonadFunctorStateT (σ : Type u_1) (m : Type u_1 → Type u_2) [inst : Monad m] :
Equations
@[always_inline]
instance StateT.instMonadExceptOfStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] (ε : Type u_1) [inst : MonadExceptOf ε m] :
Equations
@[inline]
def ForM.forIn {m : Type u_1 → Type u_2} {β : Type u_1} {ρ : Type u_3} {α : Type u_4} [inst : Monad m] [inst : ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β) (f : αβm (ForInStep β)) :
m β

Adapter to create a ForIn instance from a ForM instance

Equations
  • One or more equations did not get rendered due to their size.
instance instMonadStateOfStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] :
Equations
  • instMonadStateOfStateT = { get := StateT.get, set := StateT.set, modifyGet := fun {α} => StateT.modifyGet }
@[always_inline]
instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [inst : Monad m] :
Equations
  • One or more equations did not get rendered due to their size.
@[always_inline]
instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [inst : MonadFinally m] [inst : Monad m] :
Equations
  • One or more equations did not get rendered due to their size.