The State monad transformer using CPS style.
instance
StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
LawfulMonad (StateCpsT σ m)
@[always_inline]
instance
StateCpsT.instMonadStateOfStateCpsT
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
MonadStateOf σ (StateCpsT σ m)
@[simp]
theorem
StateCpsT.runK_pure
{α : Type u}
{σ : Type u}
{β : Type u}
{m : Type u → Type 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 u → Type v}
(s : σ)
(k : σ → σ → m β)
:
StateCpsT.runK get s k = k s s
@[simp]
theorem
StateCpsT.runK_set
{σ : Type u}
{β : Type u}
{m : Type u → Type v}
(s : σ)
(s' : σ)
(k : PUnit → σ → m β)
:
StateCpsT.runK (set s') s k = k PUnit.unit s'
@[simp]
theorem
StateCpsT.runK_modify
{σ : Type u}
{β : Type u}
{m : Type u → Type v}
(f : σ → σ)
(s : σ)
(k : PUnit → σ → m β)
:
StateCpsT.runK (modify f) s k = k PUnit.unit (f s)
@[simp]
theorem
StateCpsT.runK_lift
{m : Type u → Type u_1}
{β : Type u}
{α : Type u}
{σ : Type u}
[Monad m]
(x : m α)
(s : σ)
(k : α → σ → m β)
:
StateCpsT.runK (StateCpsT.lift x) s k = do
let x ← x
k x s
@[simp]
theorem
StateCpsT.runK_monadLift
{m : Type u → Type u_1}
{n : Type u → Type u_2}
{α : Type u}
{β : Type u}
{σ : Type u}
[Monad m]
[MonadLiftT n m]
(x : n α)
(s : σ)
(k : α → σ → m β)
:
StateCpsT.runK (monadLift x) s k = do
let x ← monadLift x
k x s
@[simp]
theorem
StateCpsT.runK_bind_pure
{m : Type u → Type u_1}
{β : Type u}
{γ : Type u}
{α : Type u}
{σ : Type u}
[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 u → Type u_1}
{β : Type u}
{γ : Type u}
{α : Type u}
{σ : Type u}
[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 u → Type u_1}
{β : Type u}
{γ : Type u}
{σ : Type u}
[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 u → Type u_1}
{β : Type u}
{γ : Type u}
{σ : Type u}
[Monad m]
(f : PUnit → StateCpsT σ m β)
(s : σ)
(s' : σ)
(k : β → σ → m γ)
:
StateCpsT.runK (set s' >>= f) s k = StateCpsT.runK (f PUnit.unit) s' k
@[simp]
theorem
StateCpsT.runK_bind_modify
{m : Type u → Type u_1}
{β : Type u}
{γ : Type u}
{σ : Type u}
[Monad m]
(f : σ → σ)
(g : PUnit → StateCpsT σ m β)
(s : σ)
(k : β → σ → m γ)
:
StateCpsT.runK (modify f >>= g) s k = StateCpsT.runK (g PUnit.unit) (f s) k
@[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)}
[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_1 → Type u_2}
{σ : Type u_1}
{α : Type u_1}
[Monad m]
(x : StateCpsT σ m α)
(s : σ)
:
StateCpsT.run' x s = StateCpsT.runK x s fun a x => pure a