Init.Control.StateCps

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

source

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

source

@[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 x => pure a

source

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

Monad (StateCpsT σ m)

Equations

StateCpsT.instMonadStateCpsT = Monad.mk

source

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

LawfulMonad (StateCpsT σ m)

Equations

@StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT = @StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT.proof_1

source

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 }

source

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

source

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

MonadLift m (StateCpsT σ m)

Equations

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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 x => pure a