mathlib3 documentation

core / init.control.except

inductive except (ε : Type u) (α : Type v) :
Type (max u v)
Instances for except
@[protected]
def except.return {ε : Type u} {α : Type v} (a : α) :
except ε α
Equations
@[protected]
def except.map {ε : Type u} {α β : Type v} (f : α β) :
except ε α except ε β
Equations
@[protected]
def except.map_error {ε ε' : Type u} {α : Type v} (f : ε ε') :
except ε α except ε' α
Equations
@[protected]
def except.bind {ε : Type u} {α β : Type v} (ma : except ε α) (f : α except ε β) :
except ε β
Equations
@[protected]
def except.to_bool {ε : Type u} {α : Type v} :
Equations
@[protected]
def except.to_option {ε : Type u} {α : Type v} :
except ε α option α
Equations
@[protected, instance]
def except.monad {ε : Type u} :
Equations
@[protected]
def except_t.return {ε : Type u} {m : Type u Type v} [monad m] {α : Type u} (a : α) :
except_t ε m α
Equations
@[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
@[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
@[protected]
def except_t.lift {ε : Type u} {m : Type u Type v} [monad m] {α : Type u} (t : m α) :
except_t ε m α
Equations
@[protected, instance]
def except_t.has_monad_lift {ε : Type u} {m : Type u Type v} [monad m] :
Equations
@[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
@[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
@[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
@[protected, instance]
def except_t.monad {ε : Type u} {m : Type u Type v} [monad m] :
Equations
@[protected]
def except_t.adapt {ε : Type u} {m : Type u Type v} [monad m] {ε' α : Type u} (f : ε ε') :
except_t ε m α except_t ε' m α
Equations
@[class]
structure monad_except (ε : out_param (Type u)) (m : Type v Type w) :
Type (max u (v+1) w)

An implementation of MonadError

Instances of this typeclass
Instances of other typeclasses for monad_except
  • monad_except.has_sizeof_inst
@[protected]
def monad_except.orelse {ε : Type u} {m : Type v Type w} [monad_except ε m] {α : Type v} (t₁ t₂ : m α) :
m α
Equations
meta def monad_except.orelse' {ε : Type u} {m : Type v Type w} [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex : bool := 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.

@[protected, instance]
def except_t.monad_except (m : Type u_1 Type u_2) (ε : out_param (Type u_1)) [monad m] :
Equations
@[class]
structure monad_except_adapter (ε ε' : out_param (Type u)) (m m' : Type u Type v) :
Type (max (u+1) v)

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 of this typeclass
Instances of other typeclasses for monad_except_adapter
  • monad_except_adapter.has_sizeof_inst
@[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'] :
Equations
@[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
@[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