Documentation

Init.Control.Option

instance instToBoolOption {α : Type u_1} :
def OptionT (m : Type u → Type v) (α : Type u) :
Instances For
    @[inline]
    def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) :
    m (Option α)
    Instances For
      def OptionT.mk {m : Type u → Type v} {α : Type u} (x : m (Option α)) :
      OptionT m α
      Instances For
        @[inline]
        def OptionT.bind {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (x : OptionT m α) (f : αOptionT m β) :
        OptionT m β
        Instances For
          @[inline]
          def OptionT.pure {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
          OptionT m α
          Instances For
            @[always_inline]
            instance OptionT.instMonadOptionT {m : Type u → Type v} [Monad m] :
            @[inline]
            def OptionT.orElse {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (y : UnitOptionT m α) :
            OptionT m α
            Instances For
              @[inline]
              def OptionT.fail {m : Type u → Type v} [Monad m] {α : Type u} :
              OptionT m α
              Instances For
                @[inline]
                def OptionT.lift {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) :
                OptionT m α
                Instances For
                  @[inline]
                  def OptionT.tryCatch {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (handle : UnitOptionT m α) :
                  OptionT m α
                  Instances For
                    instance instMonadControlOptionT {m : Type u_1 → Type u_2} [Monad m] :