The State monad transformer using CPS style.
@[inline]
def
StateCpsT.runK
{β : Type u}
{α : Type u}
{σ : Type u}
{m : Type u → Type v}
(x : StateCpsT σ m α)
(s : σ)
(k : α → σ → m β)
:
m β
Equations
- StateCpsT.runK x s k = x β s k
Instances For
@[inline]
def
StateCpsT.run
{α : Type u}
{σ : Type u}
{m : Type u → Type v}
[Monad m]
(x : StateCpsT σ m α)
(s : σ)
:
m (α × σ)
Equations
- StateCpsT.run x s = StateCpsT.runK x s fun (a : α) (s : σ) => pure (a, s)
Instances For
@[inline]
def
StateCpsT.run'
{α : Type u}
{σ : Type u}
{m : Type u → Type v}
[Monad m]
(x : StateCpsT σ m α)
(s : σ)
:
m α
Equations
- StateCpsT.run' x s = StateCpsT.runK x s fun (a : α) (x : σ) => pure a
Instances For
instance
StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
LawfulMonad (StateCpsT σ m)
Equations
- ⋯ = ⋯
@[always_inline]
instance
StateCpsT.instMonadStateOfStateCpsT
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
MonadStateOf σ (StateCpsT σ m)
Equations
- One or more equations did not get rendered due to their size.
@[inline]
def
StateCpsT.lift
{m : Type u_1 → Type u_2}
{α : Type u_1}
{σ : Type u_1}
[Monad m]
(x : m α)
:
StateCpsT σ m α
Equations
- StateCpsT.lift x✝ x s k = do let x ← x✝ k x s
Instances For
@[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