Documentation

Init.Control.State

noncomputable def StateT (σ : Type u) (m : Type uType v) (α : Type u) :
Type (max u v)
Equations
@[inline]
def StateT.run {σ : Type u} {m : Type uType v} {α : Type u} (x : StateT σ m α) (s : σ) :
m (α × σ)
Equations
@[inline]
def StateT.run' {σ : Type u} {m : Type uType v} [inst : Functor m] {α : Type u} (x : StateT σ m α) (s : σ) :
m α
Equations
noncomputable def StateM (σ : Type u) (α : Type u) :
Type u
Equations
noncomputable instance instSubsingletonStateM {σ : Type u_1} {α : Type u_1} [inst : Subsingleton σ] [inst : Subsingleton α] :
Equations
@[inline]
def StateT.pure {σ : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} (a : α) :
StateT σ m α
Equations
@[inline]
def StateT.bind {σ : Type u} {m : Type uType 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 uType 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)
instance StateT.instMonadStateT {σ : Type u} {m : Type uType v} [inst : Monad m] :
Monad (StateT σ m)
Equations
  • StateT.instMonadStateT = Monad.mk
@[inline]
def StateT.orElse {σ : Type u} {m : Type uType v} [inst : Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : UnitStateT σ m α) :
StateT σ m α
Equations
@[inline]
def StateT.failure {σ : Type u} {m : Type uType v} [inst : Alternative m] {α : Type u} :
StateT σ m α
Equations
instance StateT.instAlternativeStateT {σ : Type u} {m : Type uType 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 uType v} [inst : Monad m] :
StateT σ m σ
Equations
@[inline]
def StateT.set {σ : Type u} {m : Type uType v} [inst : Monad m] :
σStateT σ m PUnit
Equations
@[inline]
def StateT.modifyGet {σ : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} (f : σα × σ) :
StateT σ m α
Equations
@[inline]
def StateT.lift {σ : Type u} {m : Type uType v} [inst : Monad m] {α : Type u} (t : m α) :
StateT σ m α
Equations
instance StateT.instMonadLiftStateT {σ : Type u} {m : Type uType v} [inst : Monad m] :
MonadLift m (StateT σ m)
Equations
  • StateT.instMonadLiftStateT = { monadLift := fun {α} => StateT.lift }
instance StateT.instMonadFunctorStateT (σ : Type u_1) (m : Type u_1Type u_2) [inst : Monad m] :
Equations
instance StateT.instMonadExceptOfStateT {σ : Type u} {m : Type uType v} [inst : Monad m] (ε : Type u_1) [inst : MonadExceptOf ε m] :
Equations
instance instMonadStateOfStateT {σ : Type u} {m : Type uType v} [inst : Monad m] :
Equations
  • instMonadStateOfStateT = { get := StateT.get, set := StateT.set, modifyGet := fun {α} => StateT.modifyGet }
instance StateT.monadControl (σ : Type u) (m : Type uType v) [inst : Monad 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 uType v} {σ : Type u} [inst : MonadFinally m] [inst : Monad m] :
Equations
  • StateT.tryFinally = { tryFinally' := fun {α β} x h s => do let discr ← tryFinally' (x s) fun x => match x with | some (a, s') => h (some a) s' | none => h none s let x : (α × σ) × β × σ := discr match x with | ((a, x), b, s'') => pure ((a, b), s'') }