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} :
exceptional α(α → exceptional β)exceptional β

meta def exceptional.return {α : Type} :
α → exceptional α

meta def exceptional.fail {α : Type} :

@[instance]