Documentation

Lake.Util.Task

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