core / init.meta.exceptional

meta inductive exceptional (α : Type) :

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

An exceptional is similar to Result in Haskell.

Remark: we use a function that produces a format object as the exception information. Motivation: the formatting object may be big, and we may create it on demand.

Instances for exceptional

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