@[inline]

def Control.Monad.Except.throwError {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] (e : ε) : ExceptT ε m α

Throw an error in ExceptT.

$$\text{throwError}(\varepsilon) : \text{ExceptT}\ \varepsilon\ m\ \alpha$$

Alias for Lean's throw.

Equations

• Control.Monad.Except.throwError e = ExceptT.mk (pure (Except.error e))

@[inline]

def Control.Monad.Except.catchError {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] (ma : ExceptT ε m α) (handler : ε → ExceptT ε m α) : ExceptT ε m α

Catch an error in ExceptT, applying a handler.

$$\text{catchError}(ma, h) : \text{ExceptT}\ \varepsilon\ m\ \alpha$$

Runs ma; if it throws error e, runs h e instead. Alias for Lean's tryCatch pattern.

Equations

• Control.Monad.Except.catchError ma handler = ExceptT.mk do let __do_lift ← ma.run match __do_lift with | Except.ok a => pure (Except.ok a) | Except.error e => (handler e).run

@[inline]

def Control.Monad.Except.liftEither {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] (ea : Except ε α) : ExceptT ε m α

Lift a pure Except value into ExceptT.

$$\text{liftEither} : \text{Except}\ \varepsilon\ \alpha \to \text{ExceptT}\ \varepsilon\ m\ \alpha$$

Equations

• Control.Monad.Except.liftEither ea = ExceptT.mk (pure ea)

@[inline]

def Control.Monad.Except.mapExceptT {m : Type (max u_1 u_2) → Type u_3} {n : Type (max u_4 u_5) → Type u_6} {ε α : Type (max u_1 u_2)} {ε' β : Type (max u_4 u_5)} (f : m (Except ε α) → n (Except ε' β)) (ma : ExceptT ε m α) : ExceptT ε' n β

Map over the inner computation and error/value types.

$$\text{mapExceptT}(f, ma) : \text{ExceptT}\ \varepsilon'\ n\ \beta$$

where $f : m\ (\text{Except}\ \varepsilon\ \alpha) \to n\ (\text{Except}\ \varepsilon'\ \beta)$.

Equations

• Control.Monad.Except.mapExceptT f ma = ExceptT.mk (f ma.run)

@[inline]

def Control.Monad.Except.withExceptT {m : Type (max u_1 u_2) → Type u_3} {ε ε' α : Type (max u_1 u_2)} [Functor m] (f : ε → ε') (ma : ExceptT ε m α) : ExceptT ε' m α

Map over the error type, leaving the value unchanged.

$$\text{withExceptT}(f, ma) : \text{ExceptT}\ \varepsilon'\ m\ \alpha$$

where $f : \varepsilon \to \varepsilon'$.

Equations

• Control.Monad.Except.withExceptT f ma = ExceptT.mk (Except.mapError f <$> ma.run)

@[inline]

def Control.Monad.Except.runExceptT {ε : Type (max u_1 u_2)} {m : Type (max u_1 u_2) → Type u_3} {α : Type (max u_1 u_2)} (ma : ExceptT ε m α) : m (Except ε α)

Unwrap an ExceptT computation.

$$\text{runExceptT} : \text{ExceptT}\ \varepsilon\ m\ \alpha \to m\ (\text{Except}\ \varepsilon\ \alpha)$$

Alias for ExceptT.run.

Equations

• Control.Monad.Except.runExceptT ma = ma.run

theorem Control.Monad.Except.runExceptT_liftEither_ok {m : Type (max u_1 u_2) → Type u_3} {α ε : Type (max u_1 u_2)} [Monad m] (a : α) : runExceptT (liftEither (Except.ok a)) = pure (Except.ok a)

runExceptT of liftEither (.ok a) yields .ok a. $$\text{runExceptT}(\text{liftEither}(\text{ok}\ a)) = \text{pure}(\text{ok}\ a)$$

theorem Control.Monad.Except.runExceptT_liftEither_error {m : Type (max u_1 u_2) → Type u_3} {ε α : Type (max u_1 u_2)} [Monad m] (e : ε) : runExceptT (liftEither (Except.error e)) = pure (Except.error e)

runExceptT of liftEither (.error e) yields .error e. $$\text{runExceptT}(\text{liftEither}(\text{error}\ e)) = \text{pure}(\text{error}\ e)$$