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
@[protected]
def option.bind {α : Type u} {β : Type v} :
option α(α → option β)option β
Equations
@[protected]
def option.map {α : Type u_1} {β : Type u_2} (f : α → β) (o : option α) :
Equations
theorem option.map_id {α : Type u_1} :
@[protected, instance]
Equations
@[protected]
def option.orelse {α : Type u} :
option αoption αoption α
Equations
@[protected, instance]
Equations
@[protected, instance]
def option.inhabited (α : Type u) :
Equations
@[protected, instance]
def option.decidable_eq {α : Type u} [d : decidable_eq α] :
Equations