mathlib3 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 = option.some z ↔ y = option.some z) → x = y
source
theorem option.eq_some_of_is_some {α : Type u} {o : option α} (h : ↥(o.is_some)) :
o = option.some (option.get h)
source
theorem option.eq_none_of_is_none {α : Type u} {o : option α} :
↥(o.is_none) → o = option.none