@[simp]
theorem
option.get_of_mem
{α : Type u_1}
{a : α}
{o : option α}
(h : ↥(o.is_some)) :
a ∈ o → option.get h = a
@[simp]
theorem
option.some_get
{α : Type u_1}
{x : option α}
(h : ↥(x.is_some)) :
option.some (option.get h) = x
@[simp]
@[simp]
theorem
option.get_or_else_of_ne_none
{α : Type u_1}
{x : option α}
(hx : x ≠ option.none)
(y : α) :
option.some (x.get_or_else y) = x
option.map f is injective if f is injective.
theorem
option.eq_none_iff_forall_not_mem
{α : Type u_1}
{o : option α} :
o = option.none ↔ ∀ (a : α), a ∉ o
@[simp]
@[simp]
@[simp]
@[simp]
theorem
option.some_bind'
{α : Type u_1}
{β : Type u_2}
(a : α)
(f : α → option β) :
(option.some a).bind f = f a
@[simp]
theorem
option.bind_eq_some
{α β : Type u_1}
{x : option α}
{f : α → option β}
{b : β} :
x >>= f = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = option.some b
@[simp]
theorem
option.bind_eq_some'
{α : Type u_1}
{β : Type u_2}
{x : option α}
{f : α → option β}
{b : β} :
x.bind f = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = option.some b
@[simp]
@[simp]
@[simp]
@[simp]
theorem
option.map_some
{α β : Type u_1}
{a : α}
{f : α → β} :
f <$> option.some a = option.some (f a)
@[simp]
@[simp]
theorem
option.map_some'
{α : Type u_1}
{β : Type u_2}
{a : α}
{f : α → β} :
option.map f (option.some a) = option.some (f a)
@[simp]
theorem
option.map_eq_some
{α β : Type u_1}
{x : option α}
{f : α → β}
{b : β} :
f <$> x = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = b
@[simp]
theorem
option.map_eq_some'
{α : Type u_1}
{β : Type u_2}
{x : option α}
{f : α → β}
{b : β} :
option.map f x = option.some b ↔ ∃ (a : α), x = option.some a ∧ f a = b
@[simp]
theorem
option.seq_some
{α β : Type u_1}
{a : α}
{f : α → β} :
option.some f <*> option.some a = option.some (f a)
@[simp]
theorem
option.some_orelse'
{α : Type u_1}
(a : α)
(x : option α) :
(option.some a).orelse x = option.some a
@[simp]
theorem
option.some_orelse
{α : Type u_1}
(a : α)
(x : option α) :
(option.some a <|> x) = option.some a
@[simp]
@[simp]
@[simp]
theorem
option.is_some_iff_exists
{α : Type u_1}
{x : option α} :
↥(x.is_some) ↔ ∃ (a : α), x = option.some a
@[simp]
theorem
option.eq_some_iff_get_eq
{α : Type u_1}
{o : option α}
{a : α} :
o = option.some a ↔ ∃ (h : ↥(o.is_some)), option.get h = a
theorem
option.ne_none_iff_exists
{α : Type u_1}
{o : option α} :
o ≠ option.none ↔ ∃ (x : α), o = option.some x
theorem
option.ne_none_iff_exists'
{α : Type u_1}
{o : option α} :
o ≠ option.none ↔ ∃ (x : α), o = ↑x
theorem
option.bex_ne_none
{α : Type u_1}
{p : option α → Prop} :
(∃ (x : option α) (H : x ≠ option.none), p x) ↔ ∃ (x : α), p (option.some x)
theorem
option.ball_ne_none
{α : Type u_1}
{p : option α → Prop} :
(∀ (x : option α), x ≠ option.none → p x) ↔ ∀ (x : α), p (option.some x)
@[simp]
theorem
option.guard_eq_some
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
{a b : α} :
option.guard p a = option.some b ↔ a = b ∧ p a
@[simp]
theorem
option.lift_or_get_choice
{α : Type u_1}
{f : α → α → α}
(h : ∀ (a b : α), f a b = a ∨ f a b = b)
(o₁ o₂ : option α) :
option.lift_or_get f o₁ o₂ = o₁ ∨ option.lift_or_get f o₁ o₂ = o₂
@[simp]
theorem
option.lift_or_get_none_left
{α : Type u_1}
{f : α → α → α}
{b : option α} :
option.lift_or_get f option.none b = b
@[simp]
theorem
option.lift_or_get_none_right
{α : Type u_1}
{f : α → α → α}
{a : option α} :
option.lift_or_get f a option.none = a
@[simp]
theorem
option.lift_or_get_some_some
{α : Type u_1}
{f : α → α → α}
{a b : α} :
option.lift_or_get f (option.some a) (option.some b) = ↑(f a b)
given an element of a : option α, a default element b : β and a function α → β, apply this
function to a if it comes from α, and return b otherwise.
Equations
- (option.some a).cases_on' n s = s a
- option.none.cases_on' n s = n