@[inline]
Equations
- Except.pure a = Except.ok a
@[inline]
Equations
- Except.map f x = match x with | Except.error err => Except.error err | Except.ok v => Except.ok (f v)
@[inline]
Equations
- Except.mapError f x = match x with | Except.error err => Except.error (f err) | 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.bind ma f = match ma with | Except.error err => Except.error err | Except.ok v => f v
@[inline]
Equations
- Except.toBool x = match x with | Except.ok x => true | Except.error x => false
@[inline]
Equations
- Except.toOption x = match x with | Except.ok a => some a | Except.error x => none
@[inline]
def
Except.tryCatch
{ε : Type u}
{α : Type u_1}
(ma : Except ε α)
(handle : ε → Except ε α)
:
Except ε α
Equations
- Except.tryCatch ma handle = match ma with | Except.ok a => Except.ok a | Except.error e => handle e
def
Except.orElseLazy
{ε : Type u}
{α : Type u_1}
(x : Except ε α)
(y : Unit → Except ε α)
:
Except ε α
Equations
- Except.orElseLazy x y = match x with | Except.ok a => Except.ok a | Except.error e => y ()
Equations
- Except.instMonadExcept = Monad.mk
@[inline]
Equations
- ExceptT.mk x = x
@[inline]
def
ExceptT.run
{ε : Type u}
{m : Type u → Type v}
{α : Type u}
(x : ExceptT ε m α)
:
m (Except ε α)
Equations
- ExceptT.run x = x
@[inline]
def
ExceptT.pure
{ε : Type u}
{m : Type u → Type v}
[inst : 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}
[inst : Monad m]
{α : Type u}
{β : Type u}
(f : α → ExceptT ε m β)
:
Equations
- ExceptT.bindCont f x = match x with | Except.ok a => f a | Except.error e => pure (Except.error e)
@[inline]
def
ExceptT.bind
{ε : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
{β : Type u}
(ma : ExceptT ε m α)
(f : α → ExceptT ε m β)
:
ExceptT ε m β
Equations
- ExceptT.bind ma f = ExceptT.mk (ma >>= ExceptT.bindCont f)
@[inline]
def
ExceptT.map
{ε : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
{β : 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}
[inst : Monad m]
{α : Type u}
(t : m α)
:
ExceptT ε m α
Equations
- ExceptT.lift t = ExceptT.mk (Except.ok <$> t)
Equations
- ExceptT.instMonadLiftExceptExceptT = { monadLift := fun {α} e => ExceptT.mk (pure e) }
@[inline]
def
ExceptT.tryCatch
{ε : Type u}
{m : Type u → Type v}
[inst : Monad m]
{α : Type u}
(ma : ExceptT ε m α)
(handle : ε → ExceptT ε m α)
:
ExceptT ε m α
Equations
- ExceptT.tryCatch ma handle = ExceptT.mk do let res ← ma match res with | Except.ok a => pure (Except.ok a) | Except.error e => handle e
instance
ExceptT.instMonadFunctorExceptT
{ε : Type u}
{m : Type u → Type v}
:
MonadFunctor m (ExceptT ε m)
@[inline]
def
ExceptT.adapt
{ε : Type u}
{m : Type u → Type v}
[inst : Monad m]
{ε' : Type u}
{α : Type u}
(f : ε → ε')
:
Equations
- ExceptT.adapt f x = ExceptT.mk (Except.mapError f <$> x)
instance
instMonadExceptOfExceptT
(m : Type u → Type v)
(ε₁ : Type u)
(ε₂ : Type u)
[inst : Monad m]
[inst : MonadExceptOf ε₁ m]
:
MonadExceptOf ε₁ (ExceptT ε₂ m)
Equations
- instMonadExceptOfExceptT m ε₁ ε₂ = { throw := fun {α} e => ExceptT.mk (throwThe ε₁ e), tryCatch := fun {α} x handle => ExceptT.mk (tryCatchThe ε₁ x handle) }
instance
instMonadExceptOfExceptT_1
(m : Type u → Type v)
(ε : Type u)
[inst : Monad m]
:
MonadExceptOf ε (ExceptT ε m)
Equations
- instMonadExceptOfExceptT_1 m ε = { throw := fun {α} e => ExceptT.mk (pure (Except.error e)), tryCatch := fun {α} => ExceptT.tryCatch }
Equations
- instMonadExceptOfExcept ε = { throw := fun {α} => Except.error, tryCatch := fun {α} => Except.tryCatch }
@[inline]
def
MonadExcept.orelse'
{ε : Type u}
{m : Type v → Type w}
[inst : MonadExcept ε m]
{α : Type v}
(t₁ : m α)
(t₂ : m α)
(useFirstEx : optParam Bool true)
:
m α
def
liftExcept
{ε : Type u_1}
{m : Type u_2 → Type u_3}
{α : Type u_2}
[inst : MonadExceptOf ε m]
[inst : Pure m]
:
Except ε α → m α
Equations
- liftExcept x = match x with | Except.ok a => pure a | Except.error e => throw e
instance
instMonadControlExceptT
(ε : Type u)
(m : Type u → Type v)
[inst : Monad m]
:
MonadControl m (ExceptT ε m)
Equations
- instMonadControlExceptT ε m = { stM := Except ε, liftWith := fun {α} f => liftM (f fun {β} x => ExceptT.run x), restoreM := fun {α} x => x }
@[inline]
def
tryFinally
{m : Type u → Type v}
{α : Type u}
{β : Type u}
[inst : MonadFinally m]
[inst : Functor m]
(x : m α)
(finalizer : m β)
:
m α
Equations
- tryFinally x finalizer = let y := tryFinally' x fun x => finalizer; (fun a => a.fst) <$> y
Equations
- Id.finally = { tryFinally' := fun {α β} x h => let a := x; let b := h (some x); pure (a, b) }
instance
ExceptT.finally
{m : Type u → Type v}
{ε : Type u}
[inst : MonadFinally m]
[inst : Monad m]
:
MonadFinally (ExceptT ε m)
Equations
- ExceptT.finally = { tryFinally' := fun {α β} x h => ExceptT.mk do let r ← tryFinally' x fun e? => match e? with | some (Except.ok a) => h (some a) | x => h none match r with | (Except.ok a, Except.ok b) => pure (Except.ok (a, b)) | (x, Except.error e) => pure (Except.error e) | (Except.error e, x) => pure (Except.error e) }