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

• x.runK 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

• x.run s = x.runK 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

• x.run' s = x.runK s fun (a : α) (x : σ) => pure a

@[always_inline]

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

Equations

• StateCpsT.instMonad = Monad.mk

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

Equations

• ⋯ = ⋯

@[always_inline]

instance StateCpsT.instMonadStateOf {σ : 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

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

Equations

• StateCpsT.instMonadLiftOfMonad = { monadLift := fun {α : Type u_1} => StateCpsT.lift }

@[simp]

theorem StateCpsT.runK_pure {α : Type u} {σ : Type u} {β : Type u} {m : Type u → Type v} (a : α) (s : σ) (k : α → σ → m β) : (pure a).runK s k = k a s

@[simp]

theorem StateCpsT.runK_get {σ : Type u} {β : Type u} {m : Type u → Type v} (s : σ) (k : σ → σ → m β) : get.runK s k = k s s

@[simp]

theorem StateCpsT.runK_set {σ : Type u} {β : Type u} {m : Type u → Type v} (s : σ) (s' : σ) (k : PUnit → σ → m β) : (set s').runK 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 β) : (modify f).runK 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.lift x).runK 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 β) : (monadLift x).runK 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 γ) : (pure a >>= f).runK s k = (f a).runK 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.lift x >>= f).runK s k = do let a ← x (f a).runK 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 γ) : (get >>= f).runK s k = (f s).runK 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 γ) : (set s' >>= f).runK s k = (f PUnit.unit).runK 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 γ) : (modify f >>= g).runK s k = (g PUnit.unit).runK (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 : σ) : x.run s = x.runK 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 : σ) : x.run' s = x.runK s fun (a : α) (x : σ) => pure a