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.27) → σ → (α → σ → m δ) → m δ)

@[inline]

def StateCpsT.runK {α σ : Type u} {m : Type u → Type v} {β : Type u} (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β

@[inline]

def StateCpsT.run {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ)

@[inline]

def StateCpsT.run' {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m α

@[always_inline]

instance StateCpsT.instMonad {σ : Type u} {m : Type u → Type v} : Monad (StateCpsT σ m)

Equations

• StateCpsT.instMonad = Monad.mk

theorem StateCpsT.instLawfulMonad {σ : Type u} {m : Type u → Type v} : LawfulMonad (StateCpsT σ m)

@[always_inline]

instance StateCpsT.instMonadStateOf {σ : Type u} {m : Type u → Type v} : MonadStateOf σ (StateCpsT σ m)

@[inline]

def StateCpsT.lift {α σ : Type u} {m : Type u → Type v} [Monad m] (x : m α) : StateCpsT σ m α

Equations

• StateCpsT.lift x✝ x s k = do let x ← x✝ k x s

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

Equations

• StateCpsT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.24} => StateCpsT.lift }

@[simp]

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

@[simp]

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

@[simp]

theorem StateCpsT.runK_set {σ : Type u} {m : Type u → Type v} {β : Type u} (s s' : σ) (k : PUnit → σ → m β) : (set s').runK s k = k PUnit.unit s'

@[simp]

theorem StateCpsT.runK_modify {σ : Type u} {m : Type u → Type v} {β : Type u} (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f).runK s k = k PUnit.unit (f s)

@[simp]

theorem StateCpsT.runK_lift {α σ : Type u} {m : Type u → Type v} {β : 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 {α σ : Type u} {m : Type u → Type v} {n : Type u → Type u_1} {β : 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 {α σ : Type u} {m : Type u → Type v} {β γ : Type u} (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k

@[simp]

theorem StateCpsT.runK_bind_lift {α σ : Type u} {m : Type u → Type v} {β γ : 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 {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k

@[simp]

theorem StateCpsT.runK_bind_set {σ : Type u} {m : Type u → Type v} {β γ : Type u} (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 {σ : Type u} {m : Type u → Type v} {β γ : Type u} (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 {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run s = x.runK s fun (a : α) (s : σ) => pure (a, s)

@[simp]

theorem StateCpsT.run'_eq {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run' s = x.runK s fun (a : α) (x : σ) => pure a