@[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
@[inline]
def
StateCpsT.run
{α : Type u}
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
(x : StateCpsT σ m α)
(s : σ)
:
m (α × σ)
Equations
- StateCpsT.run x s = StateCpsT.runK x s fun a s => pure (a, s)
@[inline]
def
StateCpsT.run'
{α : Type u}
{σ : Type u}
{m : Type u → Type v}
[inst : Monad m]
(x : StateCpsT σ m α)
(s : σ)
:
m α
Equations
- StateCpsT.run' x s = StateCpsT.runK x s fun a s => pure a
Equations
- StateCpsT.instMonadStateCpsT = Monad.mk
noncomputable instance
StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
LawfulMonad (StateCpsT σ m)
instance
StateCpsT.instMonadStateOfStateCpsT
{σ : Type u_1}
{m : Type u_1 → Type u_2}
:
MonadStateOf σ (StateCpsT σ m)
Equations
- StateCpsT.instMonadStateOfStateCpsT = { get := fun δ s k => k s s, set := fun s δ x k => k PUnit.unit s, modifyGet := fun {α} f x s k => let x_1 := f s; match x_1 with | (a, s) => k a s }
@[inline]
def
StateCpsT.lift
{m : Type u_1 → Type u_2}
{α : Type u_1}
{σ : Type u_1}
[inst : Monad m]
(x : m α)
:
StateCpsT σ m α
Equations
- StateCpsT.lift x x s k = do let a ← x k a s
@[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}
[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 u → Type u_1}
{n : Type u → Type 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 u → Type 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 u → Type 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 u → Type 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 u → Type u_1}
{β : Type u}
{γ : Type u}
{σ : Type u}
[inst : 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}
[inst : 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)}
[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_1 → Type 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 s => pure a