Documentation

Init.Data.Option.Instances

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

        Map a monadic function which returns Unit over an Option.

        Equations
        • x✝.forM x = match x✝, x with | none, x => pure () | some a, f => f a
        Instances For
          instance Option.instForM {m : TypeType u_1} {α : Type u_2} :
          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.