Documentation

Init.Data.Option.Basic

instance Option.instDecidableEqOption :
{α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α)
Equations
  • Option.instDecidableEqOption = Option.decEqOption✝
instance Option.instBEqOption :
{α : Type u_1} → [inst : BEq α] → BEq (Option α)
Equations
  • Option.instBEqOption = { beq := Option.beqOption✝ }
def Option.toMonad {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [Alternative m] :
Option αm α
Equations
Instances For
    @[inline]
    def Option.toBool {α : Type u_1} :
    Option αBool
    Equations
    Instances For
      @[inline]
      def Option.isSome {α : Type u_1} :
      Option αBool
      Equations
      Instances For
        @[inline]
        def Option.isNone {α : Type u_1} :
        Option αBool
        Equations
        Instances For
          @[inline]
          def Option.isEqSome {α : Type u_1} [BEq α] :
          Option ααBool
          Equations
          Instances For
            @[inline]
            def Option.bind {α : Type u_1} {β : Type u_2} :
            Option α(αOption β)Option β
            Equations
            Instances For
              @[inline]
              def Option.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm β) (o : Option α) :
              m (Option β)
              Equations
              Instances For
                theorem Option.map_id {α : Type u_1} :
                @[inline]
                def Option.filter {α : Type u_1} (p : αBool) :
                Option αOption α
                Equations
                Instances For
                  @[inline]
                  def Option.all {α : Type u_1} (p : αBool) :
                  Option αBool
                  Equations
                  Instances For
                    @[inline]
                    def Option.any {α : Type u_1} (p : αBool) :
                    Option αBool
                    Equations
                    Instances For
                      @[macro_inline]
                      def Option.orElse {α : Type u_1} :
                      Option α(UnitOption α)Option α
                      Equations
                      Instances For
                        instance Option.instOrElseOption {α : Type u_1} :
                        Equations
                        • Option.instOrElseOption = { orElse := Option.orElse }
                        @[inline]
                        def Option.lt {α : Type u_1} (r : ααProp) :
                        Option αOption αProp
                        Equations
                        Instances For
                          instance Option.instDecidableRelOptionLt {α : Type u_1} (r : ααProp) [s : DecidableRel r] :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          def Option.merge {α : Type u_1} (fn : ααα) :
                          Option αOption αOption α

                          Take a pair of options and if they are both some, apply the given fn to produce an output. Otherwise act like orElse.

                          Equations
                          Instances For
                            @[simp]
                            theorem Option.getD_none :
                            ∀ {α : Type u_1} {a : α}, Option.getD none a = a
                            @[simp]
                            theorem Option.getD_some :
                            ∀ {α : Type u_1} {a b : α}, Option.getD (some a) b = a
                            @[simp]
                            theorem Option.map_none' {α : Type u_1} {β : Type u_2} (f : αβ) :
                            Option.map f none = none
                            @[simp]
                            theorem Option.map_some' {α : Type u_1} {β : Type u_2} (a : α) (f : αβ) :
                            Option.map f (some a) = some (f a)
                            @[simp]
                            theorem Option.none_bind {α : Type u_1} {β : Type u_2} (f : αOption β) :
                            Option.bind none f = none
                            @[simp]
                            theorem Option.some_bind {α : Type u_1} {β : Type u_2} (a : α) (f : αOption β) :
                            Option.bind (some a) f = f a
                            @[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
                              @[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.join {α : Type u_1} (x : Option (Option α)) :

                                          Flatten an Option of Option, a specialization of joinM.

                                          Equations
                                          Instances For
                                            @[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
                                                        instance instLTOption {α : Type u_1} [LT α] :
                                                        LT (Option α)
                                                        Equations
                                                        • instLTOption = { lt := Option.lt fun (x x_1 : α) => x < x_1 }
                                                        @[always_inline]
                                                        Equations
                                                        @[always_inline]
                                                        Equations
                                                        @[always_inline]
                                                        Equations
                                                        def liftOption {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] :
                                                        Option αm α
                                                        Equations
                                                        Instances For
                                                          @[inline]
                                                          def Option.tryCatch {α : Type u_1} (x : Option α) (handle : UnitOption α) :
                                                          Equations
                                                          Instances For
                                                            Equations