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

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.instForMOfMonad {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] : ForM m (Option α) α

Equations

• Option.instForMOfMonad = { forM := Option.forM }

instance Option.instForIn'InferInstanceMembershipOfMonad {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] : ForIn' m (Option α) α inferInstance

Equations

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