mathlib3 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 ε α

Instances for except

except.has_sizeof_inst
except.monad

@[protected]

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

except ε α

Equations

except.return a = except.ok a

@[protected]

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

except ε α → except ε β

Equations

except.map f (except.ok v) = except.ok (f v)
except.map f (except.error err) = except.error err

@[protected]

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

except ε α → except ε' α

Equations

except.map_error f (except.ok v) = except.ok v
except.map_error f (except.error err) = except.error (f err)

@[protected]

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

except ε β

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

@[protected]

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

except ε α → bool

Equations

(except.ok _x).to_bool = bool.tt
(except.error _x).to_bool = bool.ff

@[protected]

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

except ε α → option α

Equations

(except.ok a).to_option = option.some a
(except.error _x).to_option = option.none

@[protected, instance]

def except.monad {ε : Type u} :

monad (except ε)

Equations

except.monad = monad.mk

structure except_t (ε : Type u) (m : Type u → Type v) (α : Type u) :

run : m (except ε α)

Instances for except_t

@[protected]

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

except_t ε m α

Equations

except_t.return a = ⟨has_pure.pure (except.ok a)⟩

@[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

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)

@[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

ma.bind f = ⟨ma.run >>= except_t.bind_cont f⟩

@[protected]

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

except_t ε m α

Equations

except_t.lift t = ⟨except.ok <$> t⟩

@[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

except_t.has_monad_lift = {monad_lift := except_t.lift _inst_1}

@[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

ma.catch handle = ⟨ma.run >>= λ (res : except ε α), except_t.catch._match_1 handle res⟩
except_t.catch._match_1 handle (except.ok a) = has_pure.pure (except.ok a)
except_t.catch._match_1 handle (except.error e) = (handle e).run

@[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

except_t.monad_map f = λ (x : except_t ε m α), ⟨f x.run⟩

@[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

except_t.monad_functor m' = {monad_map := except_t.monad_map _inst_2}

@[protected, instance]

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

monad (except_t ε m)

Equations

except_t.monad = monad.mk

@[protected]

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

except_t ε m α → except_t ε' m α

Equations

except_t.adapt f = λ (x : except_t ε m α), ⟨except.map_error f <$> x.run⟩

@[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 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

monad_except.orelse t₁ t₂ = monad_except.catch t₁ (λ (_x : ε), t₂)

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] :

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]

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 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'] :

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)}

@[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

except_t.monad_except_adapter = {adapt_except := λ (α : Type u), except_t.adapt}

@[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

except_t.monad_run ε m out = {run := λ (α : Type u_1), monad_run.run ∘ except_t.run}