def Control.Exception.try' {α : Type} (action : IO α) : IO (Data.Either String α)

Try an action, catching IO errors into Either String α.

$$\text{try'} : \text{IO}\ \alpha \to \text{IO}\ (\text{Either}\ \text{String}\ \alpha)$$

On success, returns Right a. On failure, returns Left (toString e).

Equations

• One or more equations did not get rendered due to their size.

def Control.Exception.catch' {α : Type} (action : IO α) (handler : String → IO α) : IO α

Catch an IO error with a handler.

$$\text{catch'} : \text{IO}\ \alpha \to (\text{String} \to \text{IO}\ \alpha) \to \text{IO}\ \alpha$$

If action succeeds, returns its result. If it throws, the stringified error is passed to handler.

Equations

• Control.Exception.catch' action handler = do let __do_lift ← liftM (EIO.toBaseIO action) match __do_lift with | Except.ok a => pure a | Except.error e => handler (toString e)

def Control.Exception.bracket {α β : Type} (acquire : IO α) (release : α → IO Unit) (use : α → IO β) : IO β

Bracket pattern: acquire a resource, use it, and release it.

$$\text{bracket} : \text{IO}\ \alpha \to (\alpha \to \text{IO}\ \text{Unit}) \to (\alpha \to \text{IO}\ \beta) \to \text{IO}\ \beta$$

Resource safety: release is always called, whether use succeeds or throws. If use throws, the original error is re-thrown after release completes.

Equations

• One or more equations did not get rendered due to their size.

def Control.Exception.finally' {α : Type} (action : IO α) (cleanup : IO Unit) : IO α

Ensure cleanup runs whether the action succeeds or fails.

$$\text{finally'} : \text{IO}\ \alpha \to \text{IO}\ \text{Unit} \to \text{IO}\ \alpha$$

Equivalent to bracket (pure ()) (fun _ => cleanup) (fun _ => action). Named finally' to avoid conflict with Lean's finally keyword.

Equations

• Control.Exception.finally' action cleanup = do let result ← liftM (EIO.toBaseIO action) cleanup match result with | Except.ok a => pure a | Except.error e => throw e

def Control.Exception.onException {α : Type} (action : IO α) (cleanup : IO Unit) : IO α

Run cleanup only if the action throws.

$$\text{onException} : \text{IO}\ \alpha \to \text{IO}\ \text{Unit} \to \text{IO}\ \alpha$$

On success, cleanup is skipped. On failure, cleanup runs then the original error is re-thrown.

Equations

• Control.Exception.onException action cleanup = do let result ← liftM (EIO.toBaseIO action) match result with | Except.ok a => pure a | Except.error e => do cleanup throw e

@[inline]

def Control.Exception.evaluate {α : Type} (a : α) : IO α

Evaluate a pure value in IO, forcing any thunks.

$$\text{evaluate} : \alpha \to \text{IO}\ \alpha$$

In Lean (strict evaluation), this is simply pure. Provided for Haskell API compatibility.

Equations

• Control.Exception.evaluate a = pure a