Documentation

Init.Data.Option.Instances

theorem Option.eq_of_eq_some {α : Type u} {x : Option α} {y : Option α} :
(∀ (z : α), x = some z y = some z)x = y
theorem Option.eq_none_of_isNone {α : Type u} {o : Option α} :
Option.isNone o = trueo = none