instance Lake.instMonadTask : Monad Task

Equations

• Lake.instMonadTask = Monad.mk

@[inline, reducible]

abbrev Lake.ETask (ε : Type u_1) (α : Type u_1) : Type u_1

Equations

• Lake.ETask ε = ExceptT ε Task

Instances For

• Lake.instBindSyncEIOBaseIOETask

@[inline, reducible]

abbrev Lake.OptionTask (α : Type u_1) : Type u_1

Equations

• Lake.OptionTask = OptionT Task

def Lake.BaseIOTask (α : Type u_1) : Type u_1

Equations

• Lake.BaseIOTask = Task

Instances For

• Lake.instApplicativeAsyncBaseIOBaseIOTask
• Lake.instAsyncBaseIOBaseIOTask
• Lake.instBindAsyncBaseIOBaseIOTask
• Lake.instBindSyncBaseIOBaseIOTask
• Lake.instMonadBaseIOTask
• Lake.instSyncBaseIOBaseIOTask

instance Lake.instMonadBaseIOTask : Monad Lake.BaseIOTask

Equations

• Lake.instMonadBaseIOTask = inferInstanceAs (Monad Task)

@[inline, reducible]

abbrev Lake.EIOTask (ε : Type u_1) (α : Type u_1) : Type u_1

Equations

• Lake.EIOTask ε = ExceptT ε Lake.BaseIOTask

Instances For

• Lake.instAsyncEIOBaseIOEIOTask
• Lake.instAwaitEIOTaskEIO
• Lake.instBindAsyncBaseIOEIOTask
• Lake.instSyncEIOBaseIOEIOTask

@[inline, reducible]

abbrev Lake.OptionIOTask (α : Type u_1) : Type u_1

Equations

• Lake.OptionIOTask = OptionT Lake.BaseIOTask

Instances For

• Lake.instAsyncOptionIOBaseIOOptionIOTask
• Lake.instAwaitOptionIOTaskOptionIO
• Lake.instBindAsyncBaseIOOptionIOTask
• Lake.instBindSyncOptionIOBaseIOOptionIOTask
• Lake.instInhabitedOptionIOTask
• Lake.instSyncOptionIOBaseIOOptionIOTask

instance Lake.instInhabitedOptionIOTask {α : Type u_1} : Inhabited (Lake.OptionIOTask α)

Equations

• Lake.instInhabitedOptionIOTask = { default := failure }