mathlib3 documentation

core / init.data.option.basic

def option.get_or_else {α : Type u} :
option α α α
Equations
def option.get {α : Type u} {o : option α} :
Equations
def option.rhoare {α : Type u} :
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
@[simp]
theorem option.map_id {α : Type u_1} :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def option.inhabited (α : Type u) :
Equations
@[protected, instance]
def option.decidable_eq {α : Type u} [d : decidable_eq α] :
Equations