Documentation

Init.Data.Option.Instances

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 = trueo = none
instance Option.instMembership {α : Type u_1} :
Equations
    @[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 α) :
    Equations
      @[simp]
      theorem Option.isNone_iff_eq_none {α : Type u_1} {o : Option α} :
      theorem Option.some_inj {α : Type u_1} {a b : α} :
      some a = some b a = b
      @[inline]
      def Option.decidableEqNone {α : Type u_1} {o : Option α} :

      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
        Instances For
          @[inline, deprecated Option.decidableEqNone (since := "2025-04-10")]
          def Option.decidable_eq_none {α : Type u_1} {o : Option α} :
          Equations
            Instances For
              instance Option.decidableForallMem {α : Type u_1} {p : αProp} [DecidablePred p] (o : Option α) :
              Decidable (∀ (a : α), a op a)
              Equations
                instance Option.decidableExistsMem {α : Type u_1} {p : αProp} [DecidablePred p] (o : Option α) :
                Decidable ( (a : α), a o p a)
                Equations
                  @[inline]
                  def Option.pbind {α : Type u_1} {β : Type u_2} (o : Option α) (f : (a : α) → o = some aOption β) :

                  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
                    Instances For
                      @[inline]
                      def Option.pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (o : Option α) :
                      (∀ (a : α), o = some ap 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
                        Instances For
                          @[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
                            Instances For
                              @[inline]
                              def Option.pfilter {α : Type u_1} (o : Option α) (p : (a : α) → o = some aBool) :

                              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
                                Instances For
                                  @[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
                                    Instances For
                                      instance Option.instForM {m : Type u_1 → Type u_2} {α : Type u_3} :
                                      ForM m (Option α) α
                                      Equations
                                        instance Option.instForIn'InferInstanceMembership {m : Type u_1 → Type u_2} {α : Type u_3} :
                                        Equations