Documentation

Init.Data.Option.Basic

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
                            instance instDecidableEqOption :
                            {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α)
                            Equations
                            • instDecidableEqOption = decEqOption✝
                            instance instBEqOption :
                            {α : Type u_1} → [inst : BEq α] → BEq (Option α)
                            Equations
                            • instBEqOption = { beq := beqOption✝ }
                            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