The State monad transformer using CPS style.

def StateCpsT (σ : Type u) (m : Type u → Type 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 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} [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} [Monad m] (x : StateCpsT σ m α) (s : σ) : m α

Equations

• StateCpsT.run' x s = StateCpsT.runK x s fun a x => pure a

@[always_inline]

instance StateCpsT.instMonadStateCpsT {σ : Type u_1} {m : Type u_1 → Type u_2} : Monad (StateCpsT σ m)

Equations

• StateCpsT.instMonadStateCpsT = Monad.mk

instance StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT {σ : Type u_1} {m : Type u_1 → Type u_2} : LawfulMonad (StateCpsT σ m)

Equations

• @StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT = @StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT.proof_1

@[always_inline]

instance StateCpsT.instMonadStateOfStateCpsT {σ : Type u_1} {m : Type u_1 → Type u_2} : MonadStateOf σ (StateCpsT σ m)

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_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

instance StateCpsT.instMonadLiftStateCpsT {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] : MonadLift m (StateCpsT σ m)

Equations

• StateCpsT.instMonadLiftStateCpsT = { monadLift := fun {α} => StateCpsT.lift }

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