theorem Option.eq_of_eq_some {α : Type u} {x y : Option α} : (∀ (z : α), x = some z ↔ y = some z) → x = y

theorem Option.eq_none_of_isNone {α : Type u} {o : Option α} : o.isNone = true → o = none

instance Option.instMembership {α : Type u_1} : Membership α (Option α)

Equations

• Option.instMembership = { mem := fun (b : Option α) (a : α) => b = some a }

@[simp]

theorem Option.mem_def {α : Type u_1} {a : α} {b : Option α} : a ∈ b ↔ b = some a

instance Option.instDecidableMemOfDecidableEq {α : Type u_1} [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o)

Equations

• Option.instDecidableMemOfDecidableEq j o = inferInstanceAs (Decidable (o = some j))

@[simp]

theorem Option.isNone_iff_eq_none {α : Type u_1} {o : Option α} : o.isNone = true ↔ o = none

theorem Option.some_inj {α : Type u_1} {a b : α} : some a = some b ↔ a = b

@[inline]

def Option.decidableEqNone {α : Type u_1} {o : Option α} : Decidable (o = none)

Equality with none is decidable even if the wrapped type does not have decidable equality.

This is not an instance because it is not definitionally equal to the standard instance of DecidableEq (Option α), which can cause problems. It can be locally bound if needed.

Try to use the Boolean comparisons Option.isNone or Option.isSome instead.

Equations

• Option.decidableEqNone = decidable_of_decidable_of_iff ⋯

@[inline, deprecated Option.decidableEqNone (since := "2025-04-10")]

def Option.decidable_eq_none {α : Type u_1} {o : Option α} : Decidable (o = none)

Equations

• Option.decidable_eq_none = Option.decidableEqNone

instance Option.decidableForallMem {α : Type u_1} {p : α → Prop} [DecidablePred p] (o : Option α) : Decidable (∀ (a : α), a ∈ o → p a)

Equations

• none.decidableForallMem = isTrue ⋯
• (some a).decidableForallMem = if h : p a then isTrue ⋯ else isFalse ⋯

instance Option.decidableExistsMem {α : Type u_1} {p : α → Prop} [DecidablePred p] (o : Option α) : Decidable (∃ (a : α), a ∈ o ∧ p a)

Equations

• none.decidableExistsMem = isFalse ⋯
• (some a).decidableExistsMem = if h : p a then isTrue ⋯ else isFalse ⋯

@[inline]

def Option.pbind {α : Type u_1} {β : Type u_2} (o : Option α) (f : (a : α) → o = some a → Option β) : Option β

Given an optional value and a function that can be applied when the value is some, returns the result of applying the function if this is possible.

The function f is partial because it is only defined for the values a : α such that o = some a. This restriction allows the function to use the fact that it can only be called when o is not none: it can relate its argument to the optional value o. Its runtime behavior is equivalent to that of Option.bind.

Examples:

def attach (v : Option α) : Option { y : α // v = some y } :=
  v.pbind fun x h => some ⟨x, h⟩

#reduce attach (some 3)

some ⟨3, ⋯⟩

#reduce attach none

none

Equations

• none.pbind x_2 = none
• (some a).pbind f = f a ⋯

@[inline]

def Option.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α) : (∀ (a : α), o = some a → p a) → Option β

Given a function from the elements of α that satisfy p to β and a proof that an optional value satisfies p if it's present, applies the function to the value.

Examples:

def attach (v : Option α) : Option { y : α // v = some y } :=
  v.pmap (fun a (h : a ∈ v) => ⟨_, h⟩) (fun _ h => h)

#reduce attach (some 3)

some ⟨3, ⋯⟩

#reduce attach none

none

Equations

• Option.pmap f none x_2 = none
• Option.pmap f (some a) H = some (f a ⋯)

@[inline]

def Option.pelim {α : Type u_1} {β : Sort u_2} (o : Option α) (b : β) (f : (a : α) → o = some a → β) : β

Given an optional value and a function that can be applied when the value is some, returns the result of applying the function if this is possible, or a fallback value otherwise.

The function f is partial because it is only defined for the values a : α such that o = some a. This restriction allows the function to use the fact that it can only be called when o is not none: it can relate its argument to the optional value o. Its runtime behavior is equivalent to that of Option.elim.

Examples:

def attach (v : Option α) : Option { y : α // v = some y } :=
  v.pelim none fun x h => some ⟨x, h⟩

#reduce attach (some 3)

some ⟨3, ⋯⟩

#reduce attach none

none

Equations

• none.pelim b f_2 = b
• (some a).pelim b f_2 = f_2 a ⋯

@[inline]

def Option.pfilter {α : Type u_1} (o : Option α) (p : (a : α) → o = some a → Bool) : Option α

Partial filter. If o : Option α, p : (a : α) → o = some a → Bool, then o.pfilter p is the same as o.filter p but p is passed the proof that o = some a.

Equations

• none.pfilter p_2 = none
• (some a).pfilter p_2 = bif p_2 a ⋯ then some a else none

@[inline]

def Option.forM {m : Type u_1 → Type u_2} {α : Type u_3} [Pure m] : Option α → (α → m PUnit) → m PUnit

Executes a monadic action on an optional value if it is present, or does nothing if there is no value.

Examples:

#eval ((some 5).forM set : StateM Nat Unit).run 0

((), 5)

#eval (none.forM (fun x : Nat => set x) : StateM Nat Unit).run 0

((), 0)

Equations

• none.forM x✝ = pure PUnit.unit
• (some a).forM x✝ = x✝ a

instance Option.instForM {m : Type u_1 → Type u_2} {α : Type u_3} : ForM m (Option α) α

Equations

• Option.instForM = { forM := fun [Monad m] => Option.forM }

instance Option.instForIn'InferInstanceMembership {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn' m (Option α) α inferInstance

Equations

• One or more equations did not get rendered due to their size.