# Documentation

## Init.Data.Option.Instances

theorem Option.eq_of_eq_some {α : Type u} {x : } {y : } :
(∀ (z : α), x = some z y = some z)x = y
theorem Option.eq_none_of_isNone {α : Type u} {o : } :
o.isNone = trueo = none
instance Option.instMembership {α : Type u_1} :
Equations
• Option.instMembership = { mem := fun (a : α) (b : ) => b = some a }
@[simp]
theorem Option.mem_def {α : Type u_1} {a : α} {b : } :
a b b = some a
instance Option.instDecidableMemOfDecidableEq {α : Type u_1} [] (j : α) (o : ) :
Equations
theorem Option.isNone_iff_eq_none {α : Type u_1} {o : } :
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 : } :
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 =
Instances For
instance Option.instDecidableForallForallMemOfDecidablePred {α : Type u_1} {p : αProp} [] (o : ) :
Decidable (∀ (a : α), a op a)
Equations
• x.instDecidableForallForallMemOfDecidablePred = match x with | none => | some a => if h : p a then else
instance Option.instDecidableExistsAndMemOfDecidablePred {α : Type u_1} {p : αProp} [] (o : ) :
Decidable (∃ (a : α), a o p a)
Equations
• x.instDecidableExistsAndMemOfDecidablePred = match x with | none => | some a => if h : p a then else
@[inline]
def Option.pbind {α : Type u_1} {β : Type u_2} (x : ) :
((a : α) → a x)

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
• x✝.pbind x = match x✝, x with | none, x => none | some a, f => f a
Instances For
@[inline]
def Option.pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (x : ) :
(∀ (a : α), a xp a)

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
Instances For
@[inline]
def Option.forM {m : TypeType u_1} {α : Type u_2} [Pure m] :
(α)

Map a monadic function which returns Unit over an Option.

Equations
• x✝.forM x = match x✝, x with | none, x => | some a, f => f a
Instances For
instance Option.instForM {m : TypeType u_1} {α : Type u_2} :
ForM m () α
Equations
• Option.instForM = { forM := fun [] => Option.forM }
instance Option.instForIn'InferInstanceMembership {m : Type u_1 → Type u_2} {α : Type u_3} :
ForIn' m () α inferInstance
Equations
• One or more equations did not get rendered due to their size.