Documentation

Std.Data.Option.Basic

@[inline]
def Option.elim {α : Type u_1} {β : Sort u_2} :
Option αβ(αβ)β

An elimination principle for Option. It is a nondependent version of Option.recOn.

Equations
  • Option.elim x✝¹ x✝ x = match x✝¹, x✝, x with | some x, x_1, f => f x | none, y, x => y
Instances For
    instance Option.instMembershipOption {α : Type u_1} :
    Equations
    • Option.instMembershipOption = { 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 α} :
    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.instForAllOptionDecidableForAllMemInstMembershipOption {α : Type u_1} {p : αProp} [DecidablePred p] (o : Option α) :
      Decidable (∀ (a : α), a op a)
      Equations
      • One or more equations did not get rendered due to their size.
      instance Option.instForAllOptionDecidableExistsAndMemInstMembershipOption {α : Type u_1} {p : αProp} [DecidablePred p] (o : Option α) :
      Decidable (∃ (a : α), a o p a)
      Equations
      • One or more equations did not get rendered due to their size.
      @[inline]
      def Option.get {α : Type u} (o : Option α) :

      Extracts the value a from an option that is known to be some a for some a.

      Equations
      Instances For
        @[inline]
        def Option.guard {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) :

        guard p a returns some a if p a holds, otherwise none.

        Equations
        Instances For
          @[inline]
          def Option.toList {α : Type u_1} :
          Option αList α

          Cast of Option to List. Returns [a] if the input is some a, and [] if it is none.

          Equations
          Instances For
            @[inline]
            def Option.toArray {α : Type u_1} :
            Option αArray α

            Cast of Option to Array. Returns [a] if the input is some a, and [] if it is none.

            Equations
            Instances For
              def Option.liftOrGet {α : Type u_1} (f : ααα) :
              Option αOption αOption α

              Two arguments failsafe function. Returns f a b if the inputs are some a and some b, and "does nothing" otherwise.

              Equations
              Instances For
                inductive Option.Rel {α : Type u_1} {β : Type u_2} (r : αβProp) :
                Option αOption βProp

                Lifts a relation α → β → Prop to a relation Option α → Option β → Prop by just adding none ~ none.

                Instances For
                  @[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
                  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.join {α : Type u_1} (x : Option (Option α)) :

                      Flatten an Option of Option, a specialization of joinM.

                      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
                        Instances For
                          instance Option.instForMOption {m : TypeType u_1} {α : Type u_2} :
                          ForM m (Option α) α
                          Equations
                          • Option.instForMOption = { forM := fun [Monad m] => Option.forM }
                          instance Option.instForIn'OptionInferInstanceMembershipInstMembershipOption {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.
                          @[inline]
                          def Option.mapA {m : Type u_1 → Type u_2} [Applicative m] {α : Type u_3} {β : Type u_1} (f : αm β) :
                          Option αm (Option β)

                          Like Option.mapM but for applicative functors.

                          Equations
                          Instances For
                            @[inline]
                            def Option.sequence {m : Type u → Type u_1} [Monad m] {α : Type u} :
                            Option (m α)m (Option α)

                            If you maybe have a monadic computation in a [Monad m] which produces a term of type α, then there is a naturally associated way to always perform a computation in m which maybe produces a result.

                            Equations
                            Instances For
                              @[inline]
                              def Option.elimM {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Monad m] (x : m (Option α)) (y : m β) (z : αm β) :
                              m β

                              A monadic analogue of Option.elim.

                              Equations
                              Instances For
                                @[inline]
                                def Option.getDM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : Option α) (y : m α) :
                                m α

                                A monadic analogue of Option.getD.

                                Equations
                                Instances For
                                  Equations
                                  @[simp]
                                  theorem Option.all_none :
                                  ∀ {α : Type u_1} {p : αBool}, Option.all p none = true
                                  @[simp]
                                  theorem Option.all_some :
                                  ∀ {α : Type u_1} {p : αBool} {x : α}, Option.all p (some x) = p x
                                  def Option.min {α : Type u_1} [Min α] :
                                  Option αOption αOption α

                                  The minimum of two optional values.

                                  Equations
                                  Instances For
                                    instance Option.instMinOption {α : Type u_1} [Min α] :
                                    Min (Option α)
                                    Equations
                                    • Option.instMinOption = { min := Option.min }
                                    @[simp]
                                    theorem Option.min_some_some {α : Type u_1} [Min α] {a : α} {b : α} :
                                    min (some a) (some b) = some (min a b)
                                    @[simp]
                                    theorem Option.min_some_none {α : Type u_1} [Min α] {a : α} :
                                    min (some a) none = some a
                                    @[simp]
                                    theorem Option.min_none_some {α : Type u_1} [Min α] {b : α} :
                                    min none (some b) = some b
                                    @[simp]
                                    theorem Option.min_none_none {α : Type u_1} [Min α] :
                                    min none none = none
                                    def Option.max {α : Type u_1} [Max α] :
                                    Option αOption αOption α

                                    The maximum of two optional values.

                                    Equations
                                    Instances For
                                      instance Option.instMaxOption {α : Type u_1} [Max α] :
                                      Max (Option α)
                                      Equations
                                      • Option.instMaxOption = { max := Option.max }
                                      @[simp]
                                      theorem Option.max_some_some {α : Type u_1} [Max α] {a : α} {b : α} :
                                      max (some a) (some b) = some (max a b)
                                      @[simp]
                                      theorem Option.max_some_none {α : Type u_1} [Max α] {a : α} :
                                      max (some a) none = some a
                                      @[simp]
                                      theorem Option.max_none_some {α : Type u_1} [Max α] {b : α} :
                                      max none (some b) = some b
                                      @[simp]
                                      theorem Option.max_none_none {α : Type u_1} [Max α] :
                                      max none none = none