This module provides specialized wrappers around ExceptT to support the do elaborator.

Specifically, the types here are used to tunnel early return, break and continue through non-algebraic higher-order effect combinators such as tryCatch.

@[reducible, inline]

abbrev EarlyReturnT (ρ : Type u_1) (m : Type u_1 → Type u_2) (α : Type u_1) : Type u_2

A wrapper around ExceptT signifying early return.

@[reducible, inline]

abbrev EarlyReturnT.return {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (r : ρ) : EarlyReturnT ρ m α

Exit a computation by returning a value r : ρ early.

@[reducible, inline]

abbrev EarlyReturn.runK {ρ α : Type u} {β : Type v} (x : Except ρ α) (ret : ρ → β) (pure : α → β) : β

A specialization of Except.casesOn.

@[reducible, inline]

abbrev BreakT (m : Type u_1 → Type u_2) (α : Type u_1) : Type u_2

A wrapper around OptionT signifying break in a loop.

@[reducible, inline]

abbrev BreakT.break {α : Type w} {m : Type w → Type x} [Monad m] : BreakT m α

Exit a loop body via break.

@[reducible, inline]

abbrev Break.runK {α : Type u} {β : Type v} (x : Option α) (breakK : Unit → β) (successK : α → β) : β

A specialization of Option.casesOn.

@[reducible, inline]

abbrev ContinueT (m : Type u_1 → Type u_2) (α : Type u_1) : Type u_2

A wrapper around OptionT signifying continue in a loop.

@[reducible, inline]

abbrev ContinueT.continue {α : Type w} {m : Type w → Type x} [Monad m] : ContinueT m α

Exit a loop body via continue.

@[reducible, inline]

abbrev Continue.runK {α : Type u} {β : Type v} (x : Option α) (continueK : Unit → β) (successK : α → β) : β

A specialization of Option.casesOn.