Documentation

Init.Control.Except

@[inline]

def Except.pure {ε : Type u} {α : Type u_1} (a : α) :

Except ε α

Equations

Except.pure a = Except.ok a

@[inline]

def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) :

Except ε α → Except ε β

Equations

Except.map f (Except.error err) = Except.error err
Except.map f (Except.ok v) = Except.ok (f v)

@[simp]

theorem Except.map_id {ε : Type u} {α : Type u_1} :

Except.map id = id

@[inline]

def Except.mapError {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') :

Except ε α → Except ε' α

Equations

Except.mapError f (Except.error err) = Except.error (f err)
Except.mapError f (Except.ok v) = Except.ok v

@[inline]

def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : α → Except ε β) :

Except ε β

Equations

(Except.error err).bind f = Except.error err
(Except.ok v).bind f = f v

@[inline]

def Except.toBool {ε : Type u} {α : Type u_1} :

Except ε α → Bool

Returns true if the value is Except.ok, false otherwise.

Equations

(Except.ok a).toBool = true
(Except.error a).toBool = false

@[reducible, inline]

abbrev Except.isOk {ε : Type u} {α : Type u_1} :

Except ε α → Bool

Equations

Except.isOk = Except.toBool

@[inline]

def Except.toOption {ε : Type u} {α : Type u_1} :

Except ε α → Option α

Equations

(Except.ok a).toOption = some a
(Except.error a).toOption = none

@[inline]

def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : ε → Except ε α) :

Except ε α

Equations

(Except.ok a).tryCatch handle = Except.ok a
(Except.error a).tryCatch handle = handle a

def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : Unit → Except ε α) :

Except ε α

Equations

(Except.ok a).orElseLazy y = Except.ok a
(Except.error a).orElseLazy y = y ()

@[always_inline]

instance Except.instMonad {ε : Type u} :

Monad (Except ε)

Equations

Except.instMonad = Monad.mk

@[inline]

def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) :

ExceptT ε m α

Equations

ExceptT.mk x = x

@[inline]

def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) :

m (Except ε α)

Equations

x.run = x

@[inline]

def ExceptT.pure {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :

ExceptT ε m α

Equations

ExceptT.pure a = ExceptT.mk (pure (Except.ok a))

@[inline]

def ExceptT.bindCont {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → ExceptT ε m β) :

Except ε α → m (Except ε β)

Equations

ExceptT.bindCont f (Except.ok a) = f a
ExceptT.bindCont f (Except.error e) = pure (Except.error e)

@[inline]

def ExceptT.bind {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) :

ExceptT ε m β

Equations

ma.bind f = ExceptT.mk (ma >>= ExceptT.bindCont f)

@[inline]

def ExceptT.map {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : ExceptT ε m α) :

ExceptT ε m β

Equations

ExceptT.map f x = ExceptT.mk do let a ← x match a with | Except.ok a => pure (Except.ok (f a)) | Except.error e => pure (Except.error e)

@[inline]

def ExceptT.lift {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) :

ExceptT ε m α

Equations

ExceptT.lift t = ExceptT.mk (Except.ok <$> t)

@[always_inline]

instance ExceptT.instMonadLiftExcept {ε : Type u} {m : Type u → Type v} [Monad m] :

MonadLift (Except ε) (ExceptT ε m)

Equations

ExceptT.instMonadLiftExcept = { monadLift := fun {α : Type ?u.29} (e : Except ε α) => ExceptT.mk (pure e) }

instance ExceptT.instMonadLift {ε : Type u} {m : Type u → Type v} [Monad m] :

MonadLift m (ExceptT ε m)

Equations

ExceptT.instMonadLift = { monadLift := fun {α : Type ?u.27} => ExceptT.lift }

@[inline]

def ExceptT.tryCatch {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) :

ExceptT ε m α

Equations

ma.tryCatch handle = ExceptT.mk do let res ← ma match res with | Except.ok a => pure (Except.ok a) | Except.error e => handle e

instance ExceptT.instMonadFunctor {ε : Type u} {m : Type u → Type v} :

MonadFunctor m (ExceptT ε m)

Equations

ExceptT.instMonadFunctor = { monadMap := fun {α : Type ?u.25} (f : {β : Type ?u.25} → m β → m β) (x : ExceptT ε m α) => f x }

@[always_inline]

instance ExceptT.instMonad {ε : Type u} {m : Type u → Type v} [Monad m] :

Monad (ExceptT ε m)

Equations

ExceptT.instMonad = Monad.mk

@[inline]

def ExceptT.adapt {ε : Type u} {m : Type u → Type v} [Monad m] {ε' α : Type u} (f : ε → ε') :

ExceptT ε m α → ExceptT ε' m α

Equations

ExceptT.adapt f x = ExceptT.mk (Except.mapError f <$> x)

@[always_inline]

instance instMonadExceptOfExceptT (m : Type u → Type v) (ε₁ ε₂ : Type u) [MonadExceptOf ε₁ m] :

MonadExceptOf ε₁ (ExceptT ε₂ m)

Equations

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

@[always_inline]

instance instMonadExceptOfExceptTOfMonad (m : Type u → Type v) (ε : Type u) [Monad m] :

MonadExceptOf ε (ExceptT ε m)

Equations

instMonadExceptOfExceptTOfMonad m ε = { throw := fun {α : Type ?u.29} (e : ε) => ExceptT.mk (pure (Except.error e)), tryCatch := fun {α : Type ?u.29} => ExceptT.tryCatch }

instance instInhabitedExceptTOfMonad {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] [Inhabited ε] :

Inhabited (ExceptT ε m α)

Equations

instInhabitedExceptTOfMonad = { default := throw default }

instance instMonadExceptOfExcept (ε : Type u_1) :

MonadExceptOf ε (Except ε)

Equations

instMonadExceptOfExcept ε = { throw := fun {α : Type ?u.14} => Except.error, tryCatch := fun {α : Type ?u.14} => Except.tryCatch }

@[inline]

def MonadExcept.orelse' {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx : Bool := true) :

m α

Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard orelse uses the second.

Equations

MonadExcept.orelse' t₁ t₂ useFirstEx = tryCatch t₁ fun (e₁ : ε) => tryCatch t₂ fun (e₂ : ε) => throw (if useFirstEx = true then e₁ else e₂)

@[inline]

def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) :

m (Except ε α)

Equations

observing x = tryCatch (do let a ← x pure (Except.ok a)) fun (ex : ε) => pure (Except.error ex)

def liftExcept {ε : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [MonadExceptOf ε m] [Pure m] :

Except ε α → m α

Equations

liftExcept (Except.ok a) = pure a
liftExcept (Except.error a) = throw a

instance instMonadControlExceptTOfMonad (ε : Type u) (m : Type u → Type v) [Monad m] :

MonadControl m (ExceptT ε m)

Equations

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

class MonadFinally (m : Type u → Type v) :

Type (max (u + 1) v)

tryFinally' {α β : Type u} : m α → (Option α → m β) → m (α × β)
tryFinally' x f runs x and then the "finally" computation f. When x succeeds with a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned. Hence tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.

Instances

@[inline]

def tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) :

m α

Execute x and then execute finalizer even if x threw an exception

Equations

tryFinally x finalizer = (fun (x : α × β) => x.fst) <$> tryFinally' x fun (x : Option α) => finalizer

@[always_inline]

instance Id.finally :

MonadFinally Id

Equations

Id.finally = { tryFinally' := fun {α β : Type ?u.11} (x : Id α) (h : Option α → Id β) => let a := x; let b := h (some x); pure (a, b) }

@[always_inline]

instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] :

MonadFinally (ExceptT ε m)

Equations

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