Documentation

Init.Control.StateCps

noncomputable def StateCpsT (σ : Type u) (m : Type uType v) (α : Type u) :
Type (max (u + 1) v)
Equations
  • StateCpsT σ m α = ((δ : Type u) → σ(ασm δ) → m δ)
@[inline]
def StateCpsT.runK {β : Type u} {α : Type u} {σ : Type u} {m : Type uType v} (x : StateCpsT σ m α) (s : σ) (k : ασm β) :
m β
Equations
@[inline]
def StateCpsT.run {α : Type u} {σ : Type u} {m : Type uType v} [inst : Monad m] (x : StateCpsT σ m α) (s : σ) :
m (α × σ)
Equations
@[inline]
def StateCpsT.run' {α : Type u} {σ : Type u} {m : Type uType v} [inst : Monad m] (x : StateCpsT σ m α) (s : σ) :
m α
Equations
instance StateCpsT.instMonadStateCpsT {σ : Type u_1} {m : Type u_1Type u_2} :
Equations
  • StateCpsT.instMonadStateCpsT = Monad.mk
instance StateCpsT.instMonadStateOfStateCpsT {σ : Type u_1} {m : Type u_1Type u_2} :
Equations
  • StateCpsT.instMonadStateOfStateCpsT = { get := fun x s k => k s s, set := fun s x x_1 k => k PUnit.unit s, modifyGet := fun {α} f x s k => match f s with | (a, s) => k a s }
@[inline]
def StateCpsT.lift {m : Type u_1Type u_2} {α : Type u_1} {σ : Type u_1} [inst : Monad m] (x : m α) :
StateCpsT σ m α
Equations
instance StateCpsT.instMonadLiftStateCpsT {m : Type u_1Type u_2} {σ : Type u_1} [inst : Monad m] :
Equations
  • StateCpsT.instMonadLiftStateCpsT = { monadLift := fun {α} => StateCpsT.lift }
@[simp]
theorem StateCpsT.runK_pure {α : Type u} {σ : Type u} {β : Type u} {m : Type uType v} (a : α) (s : σ) (k : ασm β) :
StateCpsT.runK (pure a) s k = k a s
@[simp]
theorem StateCpsT.runK_get {σ : Type u} {β : Type u} {m : Type uType v} (s : σ) (k : σσm β) :
StateCpsT.runK get s k = k s s
@[simp]
theorem StateCpsT.runK_set {σ : Type u} {β : Type u} {m : Type uType v} (s : σ) (s' : σ) (k : PUnitσm β) :
@[simp]
theorem StateCpsT.runK_modify {σ : Type u} {β : Type u} {m : Type uType v} (f : σσ) (s : σ) (k : PUnitσm β) :
@[simp]
theorem StateCpsT.runK_lift {m : Type uType u_1} {β : Type u} {α : Type u} {σ : Type u} [inst : Monad m] (x : m α) (s : σ) (k : ασm β) :
StateCpsT.runK (StateCpsT.lift x) s k = do let a ← x k a s
@[simp]
theorem StateCpsT.runK_monadLift {m : Type uType u_1} {n : Type uType u_2} {α : Type u} {β : Type u} {σ : Type u} [inst : Monad m] [inst : MonadLiftT n m] (x : n α) (s : σ) (k : ασm β) :
StateCpsT.runK (monadLift x) s k = do let a ← monadLift x k a s
@[simp]
theorem StateCpsT.runK_bind_pure {m : Type uType u_1} {β : Type u} {γ : Type u} {α : Type u} {σ : Type u} [inst : Monad m] (a : α) (f : αStateCpsT σ m β) (s : σ) (k : βσm γ) :
StateCpsT.runK (pure a >>= f) s k = StateCpsT.runK (f a) s k
@[simp]
theorem StateCpsT.runK_bind_lift {m : Type uType u_1} {β : Type u} {γ : Type u} {α : Type u} {σ : Type u} [inst : Monad m] (x : m α) (f : αStateCpsT σ m β) (s : σ) (k : βσm γ) :
StateCpsT.runK (StateCpsT.lift x >>= f) s k = do let a ← x StateCpsT.runK (f a) s k
@[simp]
theorem StateCpsT.runK_bind_get {m : Type uType u_1} {β : Type u} {γ : Type u} {σ : Type u} [inst : Monad m] (f : σStateCpsT σ m β) (s : σ) (k : βσm γ) :
StateCpsT.runK (get >>= f) s k = StateCpsT.runK (f s) s k
@[simp]
theorem StateCpsT.runK_bind_set {m : Type uType u_1} {β : Type u} {γ : Type u} {σ : Type u} [inst : Monad m] (f : PUnitStateCpsT σ m β) (s : σ) (s' : σ) (k : βσm γ) :
@[simp]
theorem StateCpsT.runK_bind_modify {m : Type uType u_1} {β : Type u} {γ : Type u} {σ : Type u} [inst : Monad m] (f : σσ) (g : PUnitStateCpsT σ m β) (s : σ) (k : βσm γ) :
@[simp]
theorem StateCpsT.run_eq {m : Type (max u_1 u_2)Type u_3} {σ : Type (max u_1 u_2)} {α : Type (max u_1 u_2)} [inst : Monad m] (x : StateCpsT σ m α) (s : σ) :
StateCpsT.run x s = StateCpsT.runK x s fun a s => pure (a, s)
@[simp]
theorem StateCpsT.run'_eq {m : Type u_1Type u_2} {σ : Type u_1} {α : Type u_1} [inst : Monad m] (x : StateCpsT σ m α) (s : σ) :
StateCpsT.run' x s = StateCpsT.runK x s fun a x => pure a