mathlib documentation

core.init.data.option.instances

source
@[instance]
def option.is_lawful_monad  :
is_lawful_monad option

source
theorem option.eq_of_eq_some {α : Type u} {x y : option α} (a : ∀ (z : α), x = some z ↔ y = some z) :
x = y

source
theorem option.eq_some_of_is_some {α : Type u} {o : option α} (h : ↥(o.is_some)) :
o = some (option.get h)

source
theorem option.eq_none_of_is_none {α : Type u} {o : option α} (a : ↥(o.is_none)) :
o = none