mathlib documentation

core / init.control.except

inductive except (ε : Type u) (α : Type v) :
Type (max u v)
  • error : Π (ε : Type u) (α : Type v), ε → except ε α
  • ok : Π (ε : Type u) (α : Type v), α → except ε α

def except.return {ε : Type u} {α : Type v} (a : α) :
except ε α

Equations
def except.map {ε : Type u} {α β : Type v} (f : α → β) :
except ε αexcept ε β

Equations
def except.map_error {ε ε' : Type u} {α : Type v} (f : ε → ε') :
except ε αexcept ε' α

Equations
def except.bind {ε : Type u} {α β : Type v} (ma : except ε α) (f : α → except ε β) :
except ε β

Equations
def except.to_bool {ε : Type u} {α : Type v} :
except ε αbool

Equations
def except.to_option {ε : Type u} {α : Type v} :
except ε αoption α

Equations
@[instance]
def except.monad {ε : Type u} :

Equations
structure except_t (ε : Type u) (m : Type uType v) (α : Type u) :
Type v

def except_t.return {ε : Type u} {m : Type uType v} [monad m] {α : Type u} (a : α) :
except_t ε m α

Equations
def except_t.bind_cont {ε : Type u} {m : Type uType v} [monad m] {α β : Type u} (f : α → except_t ε m β) :
except ε αm (except ε β)

Equations
def except_t.bind {ε : Type u} {m : Type uType v} [monad m] {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) :
except_t ε m β

Equations
def except_t.lift {ε : Type u} {m : Type uType v} [monad m] {α : Type u} (t : m α) :
except_t ε m α

Equations
@[instance]
def except_t.has_monad_lift {ε : Type u} {m : Type uType v} [monad m] :

Equations
def except_t.catch {ε : Type u} {m : Type uType v} [monad m] {α : Type u} (ma : except_t ε m α) (handle : ε → except_t ε m α) :
except_t ε m α

Equations
def except_t.monad_map {ε : Type u} {m : Type uType v} [monad m] {m' : Type uType u_1} [monad m'] {α : Type u} (f : Π {α : Type u}, m αm' α) :
except_t ε m αexcept_t ε m' α

Equations
@[instance]
def except_t.monad_functor {ε : Type u} {m : Type uType v} [monad m] (m' : Type uType v) [monad m'] :
monad_functor m m' (except_t ε m) (except_t ε m')

Equations
@[instance]
def except_t.monad {ε : Type u} {m : Type uType v} [monad m] :

Equations
def except_t.adapt {ε : Type u} {m : Type uType v} [monad m] {ε' α : Type u} (f : ε → ε') :
except_t ε m αexcept_t ε' m α

Equations
@[class]
structure monad_except (ε : out_param (Type u)) (m : Type vType w) :
Type (max u (v+1) w)
  • throw : Π {α : Type ?}, ε → m α
  • catch : Π {α : Type ?}, m α(ε → m α)m α

An implementation of MonadError

Instances
def monad_except.orelse {ε : Type u} {m : Type vType w} [monad_except ε m] {α : Type v} (t₁ t₂ : m α) :
m α

Equations
meta def monad_except.orelse' {ε : Type u} {m : Type vType 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.

@[instance]
def except_t.monad_except (m : Type u_1Type u_2) (ε : out_param (Type u_1)) [monad m] :

Equations
@[class]
structure monad_except_adapter (ε ε' : out_param (Type u)) (m m' : Type uType 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 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' α)

Instances
@[instance]
def monad_except_adapter_trans {ε ε' : Type u} {m m' n n' : Type uType v} [monad_functor m m' n n'] [monad_except_adapter ε ε' m m'] :

Equations
@[instance]
def except_t.monad_except_adapter {ε ε' : Type u} {m : Type uType v} [monad m] :
monad_except_adapter ε ε' (except_t ε m) (except_t ε' m)

Equations
@[instance]
def except_t.monad_run (ε : Type u_1) (m : Type u_1Type u_2) (out : out_param (Type u_1Type u_2)) [monad_run out m] :
monad_run (λ (α : Type u_1), out (except ε α)) (except_t ε m)

Equations