Documentation

Init.Control.Option

instance instToBoolOption {α : Type u_1} :
Equations
    def OptionT (m : Type u → Type v) (α : Type u) :

    Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a failure occurred.

    Equations
      Instances For
        @[inline]
        def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) :
        m (Option α)

        Executes an action that might fail in the underlying monad m, returning none in case of failure.

        Equations
          Instances For
            def OptionT.mk {m : Type u → Type v} {α : Type u} (x : m (Option α)) :
            OptionT m α

            Converts an action that returns an Option into one that might fail, with none indicating failure.

            Equations
              Instances For
                @[inline]
                def OptionT.bind {m : Type u → Type v} [Monad m] {α β : Type u} (x : OptionT m α) (f : αOptionT m β) :
                OptionT m β

                Sequences two potentially-failing actions. The second action is run only if the first succeeds.

                Equations
                  Instances For
                    @[inline]
                    def OptionT.pure {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
                    OptionT m α

                    Succeeds with the provided value.

                    Equations
                      Instances For
                        @[always_inline]
                        instance OptionT.instMonad {m : Type u → Type v} [Monad m] :
                        Equations
                          instance OptionT.instInhabitedOfPure {α : Type u} {m : Type u → Type v} [Pure m] :
                          Equations
                            @[inline]
                            def OptionT.orElse {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (y : UnitOptionT m α) :
                            OptionT m α

                            Recovers from failures. Typically used via the <|> operator.

                            Equations
                              Instances For
                                @[inline]
                                def OptionT.fail {m : Type u → Type v} [Monad m] {α : Type u} :
                                OptionT m α

                                A recoverable failure.

                                Equations
                                  Instances For
                                    instance OptionT.instAlternative {m : Type u → Type v} [Monad m] :
                                    Equations
                                      @[inline]
                                      def OptionT.lift {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) :
                                      OptionT m α

                                      Converts a computation from the underlying monad into one that could fail, even though it does not.

                                      This function is typically implicitly accessed via a MonadLiftT instance as part of automatic lifting.

                                      Equations
                                        Instances For
                                          instance OptionT.instMonadLift {m : Type u → Type v} [Monad m] :
                                          Equations
                                            instance OptionT.instMonadFunctor {m : Type u → Type v} :
                                            Equations
                                              @[inline]
                                              def OptionT.tryCatch {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (handle : UnitOptionT m α) :
                                              OptionT m α

                                              Handles failures by treating them as exceptions of type Unit.

                                              Equations
                                                Instances For
                                                  instance OptionT.instMonadExceptOf {m : Type u → Type v} (ε : Type u) [MonadExceptOf ε m] :
                                                  Equations
                                                    instance instMonadControlOptionTOfMonad {m : Type u_1 → Type u_2} [Monad m] :
                                                    Equations