@[reducible, inline, deprecated Option.get!_eq_getD]
abbrev
Option.get!_eq_getD_default
{α : Type u_1}
[Inhabited α]
(o : Option α)
:
o.get! = o.getD default
Instances For
@[simp]
@[simp]
theorem
Option.map_eq_none'
{α✝ : Type u_1}
{x : Option α✝}
{α✝¹ : Type u_2}
{f : α✝ → α✝¹}
:
Option.map f x = none ↔ x = none
@[simp]
theorem
Option.isSome_map'
{α : Type u_1}
{α✝ : Type u_2}
{f : α → α✝}
{x : Option α}
:
(Option.map f x).isSome = x.isSome
@[simp]
theorem
Option.isNone_map'
{α : Type u_1}
{α✝ : Type u_2}
{f : α → α✝}
{x : Option α}
:
(Option.map f x).isNone = x.isNone
theorem
Option.map_eq_bind
{α : Type u_1}
{α✝ : Type u_2}
{f : α → α✝}
{x : Option α}
:
Option.map f x = x.bind (some ∘ f)
theorem
Option.map_congr
{α : Type u_1}
{α✝ : Type u_2}
{f g : α → α✝}
{x : Option α}
(h : ∀ (a : α), a ∈ x → f a = g a)
:
Option.map f x = Option.map g x
theorem
Option.get_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{o : Option α}
{h : (Option.map f o).isSome = true}
:
(Option.map f o).get h = f (o.get ⋯)
@[simp]
theorem
Option.map_map
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
(h : β → γ)
(g : α → β)
(x : Option α)
:
Option.map h (Option.map g x) = Option.map (h ∘ g) x
theorem
Option.comp_map
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
(h : β → γ)
(g : α → β)
(x : Option α)
:
Option.map (h ∘ g) x = Option.map h (Option.map g x)
@[simp]
theorem
Option.map_comp_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : β → γ)
:
Option.map g ∘ Option.map f = Option.map (g ∘ f)
theorem
Option.mem_map_of_mem
{α : Type u_1}
{β : Type u_2}
{x : Option α}
{a : α}
(g : α → β)
(h : a ∈ x)
:
g a ∈ Option.map g x
@[simp]
theorem
Option.map_if
{α : Type u_1}
{β : Type u_2}
{c : Prop}
{a : α}
{f : α → β}
[Decidable c]
:
Option.map f (if c then some a else none) = if c then some (f a) else none
@[simp]
theorem
Option.map_dif
{α : Type u_1}
{β : Type u_2}
{c : Prop}
{f : α → β}
[Decidable c]
{a : c → α}
:
Option.map f (if h : c then some (a h) else none) = if h : c then some (f (a h)) else none
theorem
Option.isSome_filter_of_isSome
{α : Type u_1}
(p : α → Bool)
(o : Option α)
(h : (Option.filter p o).isSome = true)
:
@[simp]
theorem
Option.all_guard
{α : Type u_1}
{q : α → Bool}
(p : α → Prop)
[DecidablePred p]
(a : α)
:
Option.all q (Option.guard p a) = (!decide (p a) || q a)
@[simp]
theorem
Option.any_guard
{α : Type u_1}
{q : α → Bool}
(p : α → Prop)
[DecidablePred p]
(a : α)
:
Option.any q (Option.guard p a) = (decide (p a) && q a)
theorem
Option.bind_map_comm
{α : Type u_1}
{β : Type u_2}
{x : Option (Option α)}
{f : α → β}
:
x.bind (Option.map f) = (Option.map (Option.map f) x).bind id
theorem
Option.bind_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → Option γ}
{x : Option α}
:
(Option.map f x).bind g = x.bind (g ∘ f)
@[simp]
theorem
Option.map_bind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → Option β}
{g : β → γ}
{x : Option α}
:
Option.map g (x.bind f) = x.bind (Option.map g ∘ f)
theorem
Option.join_map_eq_map_join
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : Option (Option α)}
:
(Option.map (Option.map f) x).join = Option.map f x.join
theorem
Option.join_join
{α : Type u_1}
{x : Option (Option (Option α))}
:
x.join.join = (Option.map Option.join x).join
theorem
Option.map_orElse
{α : Type u_1}
{α✝ : Type u_2}
{f : α → α✝}
{x y : Option α}
:
Option.map f (x <|> y) = (Option.map f x <|> Option.map f y)
@[simp]
@[simp]
theorem
Option.guard_isSome
{α✝ : Type u_1}
{p : α✝ → Prop}
{a : α✝}
[DecidablePred p]
:
(Option.guard p a).isSome = true ↔ p a
@[simp]
theorem
Option.guard_eq_none
{α✝ : Type u_1}
{p : α✝ → Prop}
{a : α✝}
[DecidablePred p]
:
Option.guard p a = none ↔ ¬p a
@[simp]
theorem
Option.guard_pos
{α✝ : Type u_1}
{p : α✝ → Prop}
{a : α✝}
[DecidablePred p]
(h : p a)
:
Option.guard p a = some a
theorem
Option.guard_congr
{α : Type u_1}
{f g : α → Prop}
[DecidablePred f]
[DecidablePred g]
(h : ∀ (a : α), f a ↔ g a)
:
@[simp]
theorem
Option.guard_false
{α : Type u_1}
:
(Option.guard fun (x : α) => False) = fun (x : α) => none
theorem
Option.guard_comp
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
[DecidablePred p]
{f : β → α}
:
Option.guard p ∘ f = Option.map f ∘ Option.guard (p ∘ f)
theorem
Option.liftOrGet_eq_or_eq
{α : Type u_1}
{f : α → α → α}
(h : ∀ (a b : α), f a b = a ∨ f a b = b)
(o₁ o₂ : Option α)
:
Option.liftOrGet f o₁ o₂ = o₁ ∨ Option.liftOrGet f o₁ o₂ = o₂
@[simp]
theorem
Option.liftOrGet_none_left
{α : Type u_1}
{f : α → α → α}
{b : Option α}
:
Option.liftOrGet f none b = b
@[simp]
theorem
Option.liftOrGet_none_right
{α : Type u_1}
{f : α → α → α}
{a : Option α}
:
Option.liftOrGet f a none = a
@[simp]
theorem
Option.liftOrGet_some_some
{α : Type u_1}
{f : α → α → α}
{a b : α}
:
Option.liftOrGet f (some a) (some b) = some (f a b)
@[simp]
@[simp]
theorem
Option.getD_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
(o : Option α)
:
(Option.map f o).getD (f x) = f (o.getD x)
An arbitrary some a
with a : α
if α
is nonempty, and otherwise none
.
Equations
- Option.choice α = if h : Nonempty α then some (Classical.choice h) else none
Instances For
theorem
Option.choice_isSome_iff_nonempty
{α : Type u_1}
:
(Option.choice α).isSome = true ↔ Nonempty α
theorem
Option.map_or'
{α✝ : Type u_1}
{o o' : Option α✝}
{α✝¹ : Type u_2}
{f : α✝ → α✝¹}
:
Option.map f (o.or o') = (Option.map f o).or (Option.map f o')
beq #
ite #
pbind #
@[simp]
theorem
Option.map_pbind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{o : Option α}
{f : (a : α) → a ∈ o → Option β}
{g : β → γ}
:
Option.map g (o.pbind f) = o.pbind fun (a : α) (h : a ∈ o) => Option.map g (f a h)
pmap #
@[simp]
theorem
Option.pmap_none
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
{f : (a : α) → p a → β}
{h : ∀ (a : α), a ∈ none → p a}
:
Option.pmap f none h = none
@[simp]
theorem
Option.pmap_isSome
{α : Type u_1}
{β : Type u_2}
{p : α → Prop}
{f : (a : α) → p a → β}
{o : Option α}
{h : ∀ (a : α), a ∈ o → p a}
:
(Option.pmap f o h).isSome = o.isSome