Documentation

Lake.Util.OptionIO

Conceptually identical to OptionT BaseIO, but practically more efficient.

Equations
Instances For
    @[inline]
    def Lake.OptionIO.mk {α : Type} (x : EIO PUnit α) :
    Equations
    Instances For
      @[inline]
      Equations
      Instances For
        @[inline]
        def Lake.OptionIO.toEIO {α : Type} (self : Lake.OptionIO α) :
        Equations
        Instances For
          @[inline]
          def Lake.OptionIO.toIO {α : Type} (f : UnitIO.Error) (self : Lake.OptionIO α) :
          IO α
          Equations
          Instances For
            @[inline]
            def Lake.OptionIO.catchFailure {α : Type} (f : UnitBaseIO α) (self : Lake.OptionIO α) :
            Equations
            Instances For
              @[inline]
              Equations
              Instances For
                @[inline]
                def Lake.OptionIO.orElse {α : Type} (self : Lake.OptionIO α) (f : UnitLake.OptionIO α) :
                Equations
                Instances For
                  Equations
                  @[always_inline]
                  Equations
                  • One or more equations did not get rendered due to their size.