Documentation

Init.Data.Option.Basic

instance Option.instDecidableEq :
{α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α)
Equations
  • Option.instDecidableEq = Option.decEqOption✝
instance Option.instBEq :
{α : Type u_1} → [inst : BEq α] → BEq (Option α)
Equations
  • Option.instBEq = { beq := Option.beqOption✝ }
def Option.getM {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] :
Option αm α

Lifts an optional value to any Alternative, sending none to failure.

Equations
  • x.getM = match x with | none => failure | some a => pure a
Instances For
    @[deprecated Option.getM]
    def Option.toMonad {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [Alternative m] :
    Option αm α
    Equations
    • Option.toMonad = Option.getM
    Instances For
      @[inline]
      def Option.isSome {α : Type u_1} :
      Option αBool

      Returns true on some x and false on none.

      Equations
      Instances For
        @[inline, deprecated Option.isSome]
        def Option.toBool {α : Type u_1} :
        Option αBool
        Equations
        • Option.toBool = Option.isSome
        Instances For
          @[inline]
          def Option.isNone {α : Type u_1} :
          Option αBool

          Returns true on none and false on some x.

          Equations
          Instances For
            @[inline]
            def Option.isEqSome {α : Type u_1} [BEq α] :
            Option ααBool

            x?.isEqSome y is equivalent to x? == some y, but avoids an allocation.

            Equations
            • x✝.isEqSome x = match x✝, x with | some a, b => a == b | none, x => false
            Instances For
              @[inline]
              def Option.bind {α : Type u_1} {β : Type u_2} :
              Option α(αOption β)Option β
              Equations
              • x✝.bind x = match x✝, x with | none, x => none | some a, f => f a
              Instances For
                @[inline]
                def Option.bindM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm (Option β)) (o : Option α) :
                m (Option β)

                Runs f on o's value, if any, and returns its result, or else returns none.

                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 β)

                  Runs a monadic function f on an optional value. If the optional value is none the function is not called.

                  Equations
                  Instances For
                    theorem Option.map_id {α : Type u_1} :
                    @[inline]
                    def Option.filter {α : Type u_1} (p : αBool) :
                    Option αOption α

                    Keeps an optional value only if it satisfies the predicate p.

                    Equations
                    Instances For
                      @[inline]
                      def Option.all {α : Type u_1} (p : αBool) :
                      Option αBool

                      Checks that an optional value satisfies a predicate p or is none.

                      Equations
                      Instances For
                        @[inline]
                        def Option.any {α : Type u_1} (p : αBool) :
                        Option αBool

                        Checks that an optional value is not none and the value satisfies a predicate p.

                        Equations
                        Instances For
                          @[macro_inline]
                          def Option.orElse {α : Type u_1} :
                          Option α(UnitOption α)Option α

                          Implementation of OrElse's <|> syntax for Option.

                          Equations
                          • x✝.orElse x = match x✝, x with | some a, x => some a | none, b => b ()
                          Instances For
                            instance Option.instOrElse {α : Type u_1} :
                            Equations
                            • Option.instOrElse = { orElse := Option.orElse }
                            @[inline]
                            def Option.lt {α : Type u_1} (r : ααProp) :
                            Option αOption αProp
                            Equations
                            Instances For
                              instance Option.instDecidableRelLt {α : Type u_1} (r : ααProp) [s : DecidableRel r] :
                              Equations
                              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 : α}, none.getD a = a
                                @[simp]
                                theorem Option.getD_some :
                                ∀ {α : Type u_1} {a b : α}, (some a).getD 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 β) :
                                none.bind f = none
                                @[simp]
                                theorem Option.some_bind {α : Type u_1} {β : Type u_2} (a : α) (f : αOption β) :
                                (some a).bind 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
                                • x✝¹.elim 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 α) :
                                  o.isSome = trueα

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

                                  Equations
                                  • x✝.get x = match x✝, x with | some x, x_1 => x
                                  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
                                      • x.toList = match x with | none => [] | some a => [a]
                                      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
                                        • x.toArray = match x with | none => #[] | some a => #[a]
                                        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
                                              • x.join = x.bind id
                                              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
                                                  • x.sequence = match x with | none => pure none | some fn => some <$> fn
                                                  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
                                                      • x.getDM y = match x with | some a => pure a | none => y
                                                      Instances For
                                                        instance Option.instLawfulBEq (α : Type u_1) [BEq α] [LawfulBEq α] :
                                                        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.instMin {α : Type u_1} [Min α] :
                                                          Min (Option α)
                                                          Equations
                                                          • Option.instMin = { 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.instMax {α : Type u_1} [Max α] :
                                                            Max (Option α)
                                                            Equations
                                                            • Option.instMax = { 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
                                                              • x.tryCatch handle = match x with | some val => x | none => handle ()
                                                              Instances For
                                                                Equations