def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v)

@[inline]

def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ)

@[inline]

def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α

@[reducible]

def StateM (σ : Type u) (α : Type u) : Type u

instance instSubsingletonStateM {σ : Type u_1} {α : Type u_1} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α)

@[inline]

def StateT.pure {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) : StateT σ m α

@[inline]

def StateT.bind {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m β

@[inline]

def StateT.map {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : α → β) (x : StateT σ m α) : StateT σ m β

@[always_inline]

instance StateT.instMonadStateT {σ : Type u} {m : Type u → Type v} [Monad m] : Monad (StateT σ m)

@[inline]

def StateT.orElse {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) : StateT σ m α

@[inline]

def StateT.failure {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} : StateT σ m α

instance StateT.instAlternativeStateT {σ : Type u} {m : Type u → Type v} [Monad m] [Alternative m] : Alternative (StateT σ m)

@[inline]

def StateT.get {σ : Type u} {m : Type u → Type v} [Monad m] : StateT σ m σ

@[inline]

def StateT.set {σ : Type u} {m : Type u → Type v} [Monad m] : σ → StateT σ m PUnit

@[inline]

def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (f : σ → α × σ) : StateT σ m α

@[inline]

def StateT.lift {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : StateT σ m α

instance StateT.instMonadLiftStateT {σ : Type u} {m : Type u → Type v} [Monad m] : MonadLift m (StateT σ m)

@[always_inline]

instance StateT.instMonadFunctorStateT (σ : Type u_1) (m : Type u_1 → Type u_2) [Monad m] : MonadFunctor m (StateT σ m)

@[always_inline]

instance StateT.instMonadExceptOfStateT {σ : Type u} {m : Type u → Type v} [Monad m] (ε : Type u_1) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m)

@[inline]

def ForM.forIn {m : Type u_1 → Type u_2} {β : Type u_1} {ρ : Type u_3} {α : Type u_4} [Monad m] [ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

Adapter to create a ForIn instance from a ForM instance

instance instMonadStateOfStateT {σ : Type u} {m : Type u → Type v} [Monad m] : MonadStateOf σ (StateT σ m)

@[always_inline]

instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m)

@[always_inline]

instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m)