Equations
- except.return a = except.ok a
Equations
- except.map f (except.ok v) = except.ok (f v)
- except.map f (except.error err) = except.error err
Equations
- except.map_error f (except.ok v) = except.ok v
- except.map_error f (except.error err) = except.error (f err)
Equations
- ma.bind f = except.bind._match_1 f ma
- except.bind._match_1 f (except.ok v) = f v
- except.bind._match_1 f (except.error err) = except.error err
Equations
- (except.ok a).to_option = option.some a
- (except.error _x).to_option = option.none
@[instance]
Equations
Equations
- except_t.return a = ⟨has_pure.pure (except.ok a)⟩
Equations
- except_t.bind_cont f (except.ok a) = (f a).run
- except_t.bind_cont f (except.error e) = has_pure.pure (except.error e)
Equations
- except_t.lift t = ⟨except.ok <$> t⟩
@[instance]
def
except_t.has_monad_lift
{ε : Type u}
{m : Type u → Type v}
[monad m] :
has_monad_lift m (except_t ε m)
Equations
- except_t.has_monad_lift = {monad_lift := except_t.lift _inst_1}
@[instance]
def
except_t.monad_functor
{ε : Type u}
{m : Type u → Type v}
[monad m]
(m' : Type u → Type v)
[monad m'] :
monad_functor m m' (except_t ε m) (except_t ε m')
Equations
- except_t.monad_functor m' = {monad_map := except_t.monad_map _inst_2}
@[instance]
Equations
Equations
- except_t.adapt f = λ (x : except_t ε m α), ⟨except.map_error f <$> x.run⟩
@[class]
- throw : Π {α : Type ?}, ε → m α
- catch : Π {α : Type ?}, m α → (ε → m α) → m α
An implementation of MonadError
def
monad_except.orelse
{ε : Type u}
{m : Type v → Type w}
[monad_except ε m]
{α : Type v} :
m α → m α → m α
Equations
- monad_except.orelse t₁ t₂ = monad_except.catch t₁ (λ (_x : ε), t₂)
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.
@[instance]
def
except_t.monad_except
(m : Type u_1 → Type u_2)
(ε : out_param (Type u_1))
[monad m] :
monad_except ε (except_t ε m)
Equations
- except_t.monad_except m ε = {throw := λ (α : Type u_1), except_t.mk ∘ has_pure.pure ∘ except.error, catch := except_t.catch _inst_1}
@[class]
- adapt_except : Π {α : Type ?}, (ε → ε') → m α → m' α
Adapt a monad stack, changing its top-most error type.
Note: This class can be seen as a simplification of the more "principled" definition
lean
class monad_except_functor (ε ε' : out_param (Type u)) (n n' : Type u → Type u) :=
(map {α : Type u} : (∀ {m : Type u → Type u} [monad m], except_t ε m α → except_t ε' m α) → n α → n' α)
@[instance]
def
monad_except_adapter_trans
{ε ε' : Type u}
{m m' n n' : Type u → Type v}
[monad_functor m m' n n']
[monad_except_adapter ε ε' m m'] :
monad_except_adapter ε ε' n n'
Equations
- monad_except_adapter_trans = {adapt_except := λ (α : Type u) (f : ε → ε'), monad_functor_t.monad_map (λ (α : Type u), monad_except_adapter.adapt_except f)}
@[instance]
def
except_t.monad_except_adapter
{ε ε' : Type u}
{m : Type u → Type v}
[monad m] :
monad_except_adapter ε ε' (except_t ε m) (except_t ε' m)
Equations
- except_t.monad_except_adapter = {adapt_except := λ (α : Type u), except_t.adapt}
@[instance]
def
except_t.monad_run
(ε : Type u_1)
(m : Type u_1 → Type u_2)
(out : out_param (Type u_1 → Type u_2))
[monad_run out m] :
Equations
- except_t.monad_run ε m out = {run := λ (α : Type u_1), monad_run.run ∘ except_t.run}