mathlib documentation

core.init.data.option.basic

def option.to_monad {m : Type → Type} [monad m] [alternative m] {A : Type} :
option Am A

Equations
def option.get_or_else {α : Type u} :
option αα → α

Equations
def option.is_some {α : Type u} :
option αbool

Equations
def option.is_none {α : Type u} :
option αbool

Equations
def option.get {α : Type u} {o : option α} :
(o.is_some) → α

Equations
def option.rhoare {α : Type u} :
boolα → option α

Equations
def option.lhoare {α : Type u} :
α → option α → α

Equations
def option.bind {α : Type u} {β : Type v} :
option α(α → option β)option β

Equations
def option.map {α : Type u_1} {β : Type u_2} :
(α → β)option αoption β

Equations
theorem option.map_id {α : Type u_1} :

@[instance]

Equations
def option.orelse {α : Type u} :
option αoption αoption α

Equations
@[instance]

Equations
@[instance]
def option.inhabited (α : Type u) :

Equations
@[instance]
def option.decidable_eq {α : Type u} [d : decidable_eq α] :

Equations