mathlib documentation

core / init.meta.exceptional

meta inductive exceptional (α : Type) :
Type

An exceptional is similar to Result in Haskell.

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