mathlib documentation

core.init.control.except

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

def except.return {ε : Type u} {α : Type v} :
α → except ε α

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

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

Equations
def except.bind {ε : Type u} {α β : Type v} :
except ε α(α → 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(Type uType v)Type uType v

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

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

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

Equations
def except_t.lift {ε : Type u} {m : Type uType v} [monad m] {α : Type u} :
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} :
except_t ε m α(ε → 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} :
(Π {α : 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} :
(ε → ε')except_t ε m αexcept_t ε' m α

Equations
@[class]
structure monad_except  :
out_param (Type u)(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} :
m αm αm α

Equations
meta def monad_except.orelse' {ε : Type u} {m : Type vType w} [monad_except ε m] {α : Type v} :
m αm α(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)out_param (Type u)(Type uType v)(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