Documentation

Init.Data.Option.Basic

def Option.toMonad {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [Alternative m] :
Option αm α
Instances For
    @[inline]
    def Option.toBool {α : Type u_1} :
    Option αBool
    Instances For
      @[inline]
      def Option.isSome {α : Type u_1} :
      Option αBool
      Instances For
        @[inline]
        def Option.isNone {α : Type u_1} :
        Option αBool
        Instances For
          @[inline]
          def Option.isEqSome {α : Type u_1} [BEq α] :
          Option ααBool
          Instances For
            @[inline]
            def Option.bind {α : Type u_1} {β : Type u_2} :
            Option α(αOption β) → Option β
            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 β)
              Instances For
                theorem Option.map_id {α : Type u_1} :
                @[inline]
                def Option.filter {α : Type u_1} (p : αBool) :
                Option αOption α
                Instances For
                  @[inline]
                  def Option.all {α : Type u_1} (p : αBool) :
                  Option αBool
                  Instances For
                    @[inline]
                    def Option.any {α : Type u_1} (p : αBool) :
                    Option αBool
                    Instances For
                      @[macro_inline]
                      def Option.orElse {α : Type u_1} :
                      Option α(UnitOption α) → Option α
                      Instances For
                        @[inline]
                        def Option.lt {α : Type u_1} (r : ααProp) :
                        Option αOption αProp
                        Instances For
                          instance Option.instDecidableRelOptionLt {α : Type u_1} (r : ααProp) [s : DecidableRel r] :
                          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.

                          Instances For
                            instance instDecidableEqOption :
                            {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α)
                            instance instBEqOption :
                            {α : Type u_1} → [inst : BEq α] → BEq (Option α)
                            instance instLTOption {α : Type u_1} [LT α] :
                            LT (Option α)
                            @[always_inline]
                            @[always_inline]
                            def liftOption {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] :
                            Option αm α
                            Instances For
                              @[inline]
                              def Option.tryCatch {α : Type u_1} (x : Option α) (handle : UnitOption α) :
                              Instances For