mathlib documentation

core / init.control.except

source
inductive except (ε : Type u) (α : Type v) :
Type (max u v)
  • error : Π (ε : Type u) (α : Type v), ε → except ε α
  • ok : Π (ε : Type u) (α : Type v), α → except ε α
source
@[protected]
def except.return {ε : Type u} {α : Type v} (a : α) :
except ε α
Equations
source
@[protected]
def except.map {ε : Type u} {α β : Type v} (f : α → β) :
except ε α → except ε β
Equations
source
@[protected]
def except.map_error {ε ε' : Type u} {α : Type v} (f : ε → ε') :
except ε α → except ε' α
Equations
source
@[protected]
def except.bind {ε : Type u} {α β : Type v} (ma : except ε α) (f : α → except ε β) :
except ε β
Equations
source
@[protected]
def except.to_bool {ε : Type u} {α : Type v} :
except ε α → bool
Equations
source
@[protected]
def except.to_option {ε : Type u} {α : Type v} :
except ε α → option α
Equations
source
@[protected, instance]
def except.monad {ε : Type u} :
monad (except ε)
Equations
source
structure except_t (ε : Type u) (m : Type u → Type v) (α : Type u) :
Type v
source
@[protected]
def except_t.return {ε : Type u} {m : Type u → Type v} [monad m] {α : Type u} (a : α) :
except_t ε m α
Equations
source
@[protected]
def except_t.bind_cont {ε : Type u} {m : Type u → Type v} [monad m] {α β : Type u} (f : α → except_t ε m β) :
except ε α → m (except ε β)
Equations
source
@[protected]
def except_t.bind {ε : Type u} {m : Type u → Type v} [monad m] {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) :
except_t ε m β
Equations
source
@[protected]
def except_t.lift {ε : Type u} {m : Type u → Type v} [monad m] {α : Type u} (t : m α) :
except_t ε m α
Equations
source
@[protected, instance]
def except_t.has_monad_lift {ε : Type u} {m : Type u → Type v} [monad m] :
has_monad_lift m (except_t ε m)
Equations
source
@[protected]
def except_t.catch {ε : Type u} {m : Type u → Type v} [monad m] {α : Type u} (ma : except_t ε m α) (handle : ε → except_t ε m α) :
except_t ε m α
Equations
source
@[protected]
def except_t.monad_map {ε : Type u} {m : Type u → Type v} [monad m] {m' : Type u → Type u_1} [monad m'] {α : Type u} (f : Π {α : Type u}, m α → m' α) :
except_t ε m α → except_t ε m' α
Equations
source
@[protected, 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
source
@[protected, instance]
def except_t.monad {ε : Type u} {m : Type u → Type v} [monad m] :
monad (except_t ε m)
Equations
source
@[protected]
def except_t.adapt {ε : Type u} {m : Type u → Type v} [monad m] {ε' α : Type u} (f : ε → ε') :
except_t ε m α → except_t ε' m α
Equations
source
@[class]
structure monad_except (ε : out_param (Type u)) (m : Type v → Type w) :
Type (max u (v+1) w)
  • throw : Π {α : Type ?}, ε → m α
  • catch : Π {α : Type ?}, m α → (ε → m α) → m α

An implementation of MonadError

Instances
source
@[protected]
def monad_except.orelse {ε : Type u} {m : Type v → Type w} [monad_except ε m] {α : Type v} (t₁ t₂ : m α) :
m α
Equations
source
meta def monad_except.orelse' {ε : Type u} {m : Type v → Type w} [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex : bool := tt) :
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.

source
@[protected, 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
source
@[class]
structure monad_except_adapter (ε ε' : out_param (Type u)) (m m' : Type u → Type v) :
Type (max (u+1) v)
  • 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

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' α)
Instances
source
@[protected, instance]
def monad_except_adapter_trans {ε ε' : Type u} {m m' n n' : Type u → Type v} [monad_except_adapter ε ε' m m'] [monad_functor m m' n n'] :
monad_except_adapter ε ε' n n'
Equations
source
@[protected, 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
source
@[protected, 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] :
monad_run (λ (α : Type u_1), out (except ε α)) (except_t ε m)
Equations