instance Lake.instMonadTask_lake : Monad Task

Equations

• Lake.instMonadTask_lake = Monad.mk

@[reducible, inline]

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

Equations

• Lake.ETask ε = ExceptT ε Task

@[reducible, inline]

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

instance Lake.instMonadBaseIOTask : Monad Lake.BaseIOTask

Equations

• Lake.instMonadBaseIOTask = inferInstanceAs (Monad Task)

instance Lake.instInhabitedBaseIOTask {α : Type u_1} [Inhabited α] : Inhabited (Lake.BaseIOTask α)

Equations

• Lake.instInhabitedBaseIOTask = inferInstance

@[reducible, inline]

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

Equations

• Lake.EIOTask ε = ExceptT ε Lake.BaseIOTask

@[reducible, inline]

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

Equations

• Lake.OptionIOTask = OptionT Lake.BaseIOTask

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

Equations

• Lake.instInhabitedOptionIOTask = { default := failure }