Documentation

Init.Control.State

@[inline]

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

m (α × σ)

Equations

x.run s = x s

@[inline]

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

m α

Equations

x.run' s = (fun (x : α × σ) => x.fst) <$> x s

@[reducible]

def StateM (σ α : Type u) :

Equations

StateM σ α = StateT σ Id α

Instances For

instance instSubsingletonStateM {σ α : 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 α

Equations

StateT.pure a s = pure (a, s)

@[inline]

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

StateT σ m β

Equations

x.bind 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} [Monad m] {α β : 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.instMonad {σ : Type u} {m : Type u → Type v} [Monad m] :

Monad (StateT σ m)

Equations

StateT.instMonad = Monad.mk

@[inline]

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

StateT σ m α

Equations

x₁.orElse x₂ s = (x₁ s <|> x₂ () s)

@[inline]

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

StateT σ m α

Equations

StateT.failure x✝ = failure

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

Alternative (StateT σ m)

Equations

StateT.instAlternative = Alternative.mk (fun {α : Type ?u.34} => StateT.failure) fun {α : Type ?u.34} => StateT.orElse

@[inline]

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

StateT σ m σ

Equations

StateT.get s = pure (s, s)

@[inline]

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

σ → StateT σ m PUnit

Equations

StateT.set s' x✝ = pure (PUnit.unit , s')

@[inline]

def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [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} [Monad m] {α : Type u} (t : m α) :

StateT σ m α

Equations

StateT.lift t s = do let a ← t pure (a, s)

instance StateT.instMonadLift {σ : Type u} {m : Type u → Type v} [Monad m] :

MonadLift m (StateT σ m)

Equations

StateT.instMonadLift = { monadLift := fun {α : Type ?u.27} => StateT.lift }

@[always_inline]

instance StateT.instMonadFunctor (σ : Type u_1) (m : Type u_1 → Type u_2) :

MonadFunctor m (StateT σ m)

Equations

StateT.instMonadFunctor σ m = { monadMap := fun {α : Type ?u.26} (f : {β : Type ?u.26} → m β → m β) (x : StateT σ m α) (s : σ) => f (x s) }

@[always_inline]

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

MonadExceptOf ε (StateT σ m)

Equations

One or more equations did not get rendered due to their size.

@[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

Equations

One or more equations did not get rendered due to their size.

instance instMonadStateOfStateTOfMonad {σ : Type u} {m : Type u → Type v} [Monad m] :

MonadStateOf σ (StateT σ m)

Equations

instMonadStateOfStateTOfMonad = { get := StateT.get, set := StateT.set, modifyGet := fun {α : Type ?u.27} => StateT.modifyGet }

@[always_inline]

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

MonadControl m (StateT σ 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} [MonadFinally m] [Monad m] :

MonadFinally (StateT σ m)

Equations

One or more equations did not get rendered due to their size.