mathlib documentation

core / init.data.option.instances

source
@[protected, instance]
def option.is_lawful_monad  :
is_lawful_monad option
source
theorem option.eq_of_eq_some {α : Type u} {x y : option α} :
(∀ (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 α} :
↥(o.is_none) → o = none