mathlib documentation

core / init.meta.exceptional

source
meta inductive exceptional (α : Type) :
Type

An exceptional is similar to Result in Haskell.

source
@[protected]
meta def exceptional.to_string {α : Type} [has_to_string α] :
exceptional α → string
source
@[protected, instance]
meta def exceptional.has_to_string {α : Type} [has_to_string α] :
has_to_string (exceptional α)
source
@[protected]
meta def exceptional.to_bool {α : Type} :
exceptional α → bool
source
@[protected]
meta def exceptional.to_option {α : Type} :
exceptional α → option α
source
@[protected]
meta def exceptional.bind {α β : Type} (e₁ : exceptional α) (e₂ : α → exceptional β) :
exceptional β
source
@[protected]
meta def exceptional.return {α : Type} (a : α) :
exceptional α
source
meta def exceptional.fail {α : Type} (f : format) :
exceptional α
source
@[protected, instance]
meta def exceptional.monad  :
monad exceptional