Init.Control.ExceptCps

source

noncomputable def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) :

Type (max (u + 1) v)

Equations

ExceptCpsT ε m α = ((β : Type u) → (α → m β) → (ε → m β) → m β)

source

@[inline]

def ExceptCpsT.run {m : Type u → Type u_1} {ε : Type u} {α : Type u} [inst : Monad m] (x : ExceptCpsT ε m α) :

m (Except ε α)

Equations

ExceptCpsT.run x = x (Except ε α) (fun a => pure (Except.ok a)) fun e => pure (Except.error e)

source

@[inline]

def ExceptCpsT.runK {m : Type u → Type u_1} {β : Type u} {ε : Type u} {α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) :

m β

Equations

ExceptCpsT.runK x s ok error = x β ok error

source

@[inline]

def ExceptCpsT.runCatch {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : ExceptCpsT α m α) :

m α

Equations

ExceptCpsT.runCatch x = x α pure pure

source

instance ExceptCpsT.instMonadExceptCpsT {ε : Type u_1} {m : Type u_1 → Type u_2} :

Monad (ExceptCpsT ε m)

Equations

ExceptCpsT.instMonadExceptCpsT = Monad.mk

source

noncomputable instance ExceptCpsT.instLawfulMonadExceptCpsTInstMonadExceptCpsT {σ : Type u_1} {m : Type u_1 → Type u_2} :

LawfulMonad (ExceptCpsT σ m)

Equations

@ExceptCpsT.instLawfulMonadExceptCpsTInstMonadExceptCpsT = @ExceptCpsT.instLawfulMonadExceptCpsTInstMonadExceptCpsT.proof_1

source

instance ExceptCpsT.instMonadExceptOfExceptCpsT {ε : Type u_1} {m : Type u_1 → Type u_2} :

MonadExceptOf ε (ExceptCpsT ε m)

Equations

ExceptCpsT.instMonadExceptOfExceptCpsT = { throw := fun {α} e x x_1 k => k e, tryCatch := fun {α} x handle x_1 k₁ k₂ => x x_1 k₁ fun e => handle e x_1 k₁ k₂ }

source

@[inline]

def ExceptCpsT.lift {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} [inst : Monad m] (x : m α) :

ExceptCpsT ε m α

Equations

ExceptCpsT.lift x x k x = x >>= k

source

instance ExceptCpsT.instMonadLiftExceptCpsT {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] :

MonadLift m (ExceptCpsT σ m)

Equations

ExceptCpsT.instMonadLiftExceptCpsT = { monadLift := fun {α} => ExceptCpsT.lift }

source

instance ExceptCpsT.instInhabitedExceptCpsT {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Inhabited ε] :

Inhabited (ExceptCpsT ε m α)

Equations

ExceptCpsT.instInhabitedExceptCpsT = { default := fun x k₁ k₂ => k₂ default }

source

@[simp]

theorem ExceptCpsT.run_pure {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {x : α} [inst : Monad m] :

ExceptCpsT.run (pure x) = pure (Except.ok x)

source

@[simp]

theorem ExceptCpsT.run_lift {m : Type u → Type u_1} {α : Type u} {ε : Type u} [inst : Monad m] (x : m α) :

ExceptCpsT.run (ExceptCpsT.lift x) = do let a ← x pure (Except.ok a)

source

@[simp]

theorem ExceptCpsT.run_throw {m : Type u_1 → Type u_2} {ε : Type u_1} {β : Type u_1} {e : ε} [inst : Monad m] :

ExceptCpsT.run (throw e) = pure (Except.error e)

source

@[simp]

theorem ExceptCpsT.run_bind_lift {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} {β : Type u_1} [inst : Monad m] (x : m α) (f : α → ExceptCpsT ε m β) :

ExceptCpsT.run (ExceptCpsT.lift x >>= f) = do let a ← x ExceptCpsT.run (f a)

source

@[simp]

theorem ExceptCpsT.run_bind_throw {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} [inst : Monad m] (e : ε) (f : α → ExceptCpsT ε m β) :

ExceptCpsT.run (throw e >>= f) = ExceptCpsT.run (throw e)

source

@[simp]

theorem ExceptCpsT.runCatch_pure {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [inst : Monad m] :

ExceptCpsT.runCatch (pure x) = pure x

source

@[simp]

theorem ExceptCpsT.runCatch_lift {m : Type u → Type u_1} {α : Type u} [inst : Monad m] [inst : LawfulMonad m] (x : m α) :

ExceptCpsT.runCatch (ExceptCpsT.lift x) = x

source

@[simp]

theorem ExceptCpsT.runCatch_throw {m : Type u_1 → Type u_2} {α : Type u_1} {a : α} [inst : Monad m] :

ExceptCpsT.runCatch (throw a) = pure a

source

@[simp]

theorem ExceptCpsT.runCatch_bind_lift {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [inst : Monad m] (x : m α) (f : α → ExceptCpsT β m β) :

ExceptCpsT.runCatch (ExceptCpsT.lift x >>= f) = do let a ← x ExceptCpsT.runCatch (f a)

source

@[simp]

theorem ExceptCpsT.runCatch_bind_throw {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_1} [inst : Monad m] (e : β) (f : α → ExceptCpsT β m β) :

ExceptCpsT.runCatch (throw e >>= f) = pure e