# 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
• = x s
@[inline]
def StateT.run' {σ : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (x : StateT σ m α) (s : σ) :
m α
Equations
• = (fun x => x.fst) <\$> x s
def StateM (σ : Type u) (α : Type u) :
Equations
instance instSubsingletonStateM {σ : Type u_1} {α : Type u_1} [inst : ] [inst : ] :
Equations
@[inline]
def StateT.pure {σ : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (a : α) :
StateT σ m α
Equations
@[inline]
def StateT.bind {σ : Type u} {m : Type u → Type v} [inst : ] {α : 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 : ] {α : 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 : ] :
Equations
@[inline]
def StateT.orElse {σ : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (x₁ : StateT σ m α) (x₂ : UnitStateT σ m α) :
StateT σ m α
Equations
@[inline]
def StateT.failure {σ : Type u} {m : Type u → Type v} [inst : ] {α : Type u} :
StateT σ m α
Equations
• = failure
instance StateT.instAlternativeStateT {σ : Type u} {m : Type u → Type v} [inst : ] [inst : ] :
Equations
• StateT.instAlternativeStateT = Alternative.mk (fun {α} => StateT.failure) fun {α} => StateT.orElse
@[inline]
def StateT.get {σ : Type u} {m : Type u → Type v} [inst : ] :
StateT σ m σ
Equations
@[inline]
def StateT.set {σ : Type u} {m : Type u → Type v} [inst : ] :
σ
Equations
@[inline]
def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (f : σα × σ) :
StateT σ m α
Equations
@[inline]
def StateT.lift {σ : Type u} {m : Type u → Type v} [inst : ] {α : Type u} (t : m α) :
StateT σ m α
Equations
• = do let a ← t pure (a, s)
instance StateT.instMonadLiftStateT {σ : Type u} {m : Type u → Type v} [inst : ] :
Equations
@[always_inline]
instance StateT.instMonadFunctorStateT (σ : Type u_1) (m : Type u_1 → Type u_2) [inst : ] :
Equations
• = { monadMap := fun {α} f x s => f (α × σ) (x s) }
@[always_inline]
instance StateT.instMonadExceptOfStateT {σ : Type u} {m : Type u → Type v} [inst : ] (ε : Type u_1) [inst : ] :
Equations
• = { throw := fun {α} => StateT.lift , tryCatch := fun {α} x c s => tryCatchThe ε (x s) fun e => c e s }
@[inline]
def ForM.forIn {m : Type u_1 → Type u_2} {β : Type u_1} {ρ : Type u_3} {α : Type u_4} [inst : ] [inst : ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β) (f : αβm ()) :
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 : ] :
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 : ] :
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 : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.