mathlib documentation

core.init.meta.exceptional

meta inductive exceptional (α : Type) :

Type

success : Π (α : Type), α → exceptional α
exception : Π (α : Type), (options → format) → exceptional α

An exceptional is similar to Result in Haskell.

meta def exceptional.to_string {α : Type} [has_to_string α] (a : exceptional α) :

@[instance]

meta def exceptional.has_to_string {α : Type} [has_to_string α] :

has_to_string (exceptional α)

meta def exceptional.to_bool {α : Type} (a : exceptional α) :

meta def exceptional.to_option {α : Type} (a : exceptional α) :

meta def exceptional.bind {α β : Type} (e₁ : exceptional α) (e₂ : α → exceptional β) :

meta def exceptional.return {α : Type} (a : α) :

meta def exceptional.fail {α : Type} (f : format) :

@[instance]

meta def exceptional.monad :

monad exceptional