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.

Equations

• EarlyReturnT ρ m α = ExceptT ρ m α

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

Equations

• EarlyReturnT.return r = throw r

@[reducible, inline]

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

A specialization of Except.casesOn.

Equations

• EarlyReturn.runK x ret pure = Except.casesOn x ret pure

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

Equations

• BreakT = OptionT

@[reducible, inline]

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

Exit a loop body via break.

Equations

• BreakT.break = failure

@[reducible, inline]

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

A specialization of Option.casesOn.

Equations

• Break.runK (some a) breakK successK = successK a
• Break.runK none breakK successK = breakK ()

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

Equations

• ContinueT = OptionT

@[reducible, inline]

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

Exit a loop body via continue.

Equations

• ContinueT.continue = failure

@[reducible, inline]

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

A specialization of Option.casesOn.

Equations

• Continue.runK x continueK successK = Option.casesOn (motive := fun (x : Option α) => Unit → β) x continueK (fun (a : α) (x : Unit) => successK a) ()