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.decidable_eq_none {α : Type u_1} {o : Option α} : Decidable (o = none)

o = 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 instance : DecidableEq Option. Try to use o.isNone or o.isSome instead.

Equations

• Option.decidable_eq_none = decidable_of_decidable_of_iff ⋯

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

Equations

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

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

Equations

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

@[inline]

def Option.pbind {α : Type u_1} {β : Type u_2} (x : Option α) : ((a : α) → a ∈ x → Option β) → Option β

Partial bind. If for some x : Option α, f : Π (a : α), a ∈ x → Option β is a partial function defined on a : α giving an Option β, where some a = x, then pbind x f h is essentially the same as bind x f but is defined only when all x = some a, using the proof to apply f.

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 → β) (x : Option α) : (∀ (a : α), a ∈ x → p a) → Option β

Partial map. If f : Π a, p a → β is a partial function defined on a : α satisfying p, then pmap f x h is essentially the same as map f x but is defined only when all members of x satisfy p, using the proof to apply f.

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 : α) → a ∈ o → β) : β

Partial elimination. If o : Option α and f : (a : α) → a ∈ o → β, then o.pelim b f is the same as o.elim b f but f is passed the proof that a ∈ o.

Equations

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

@[inline]

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

Map a monadic function which returns Unit over an Option.

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.