Documentation

Lake.Util.Task

@[inline, reducible]
abbrev Lake.ETask (ε : Type u_1) (α : Type u_1) :
Type u_1
Equations
Instances For
    @[inline, reducible]
    abbrev Lake.OptionTask (α : Type u_1) :
    Type u_1
    Equations
    Instances For
      def Lake.BaseIOTask (α : Type u_1) :
      Type u_1
      Equations
      Instances For
        @[inline, reducible]
        abbrev Lake.EIOTask (ε : Type u_1) (α : Type u_1) :
        Type u_1
        Equations
        Instances For
          @[inline, reducible]
          abbrev Lake.OptionIOTask (α : Type u_1) :
          Type u_1
          Equations
          Instances For
            Equations
            • Lake.instInhabitedOptionIOTask = { default := failure }