Documentation

Lake.Util.OptionIO

source
def Lake.OptionIO :
Type → Type

Conceptually identical to OptionT BaseIO, but practically more efficient.

Instances For
    source
    instance Lake.instMonadOptionIO :
    Monad Lake.OptionIO
    source
    instance Lake.instMonadLiftBaseIOOptionIO :
    MonadLift BaseIO Lake.OptionIO
    source
    @[inline]
    def Lake.OptionIO.mk {α : Type} (x : EIO PUnit α) :
    Lake.OptionIO α
    Instances For
      source
      @[inline]
      def Lake.OptionIO.toBaseIO {α : Type} (self : Lake.OptionIO α) :
      BaseIO (Option α)
      Instances For
        source
        @[inline]
        def Lake.OptionIO.toEIO {α : Type} (self : Lake.OptionIO α) :
        EIO PUnit α
        Instances For
          source
          @[inline]
          def Lake.OptionIO.toIO {α : Type} (f : Unit → IO.Error) (self : Lake.OptionIO α) :
          IO α
          Instances For
            source
            @[inline]
            def Lake.OptionIO.catchFailure {α : Type} (f : Unit → BaseIO α) (self : Lake.OptionIO α) :
            BaseIO α
            Instances For
              source
              @[inline]
              def Lake.OptionIO.failure {α : Type} :
              Lake.OptionIO α
              Instances For
                source
                @[inline]
                def Lake.OptionIO.orElse {α : Type} (self : Lake.OptionIO α) (f : Unit → Lake.OptionIO α) :
                Lake.OptionIO α
                Instances For
                  source
                  instance Lake.OptionIO.instAlternativeOptionIO :
                  Alternative Lake.OptionIO
                  source
                  @[always_inline]
                  instance Lake.OptionIO.OptionIO.finally :
                  MonadFinally Lake.OptionIO
                  source
                  def Lake.OptionIO.asTask {α : Type} (self : Lake.OptionIO α) (prio : optParam Task.Priority Task.Priority.dedicated) :
                  BaseIO (Task (Option α))
                  Instances For