@[implicit_reducible]

instance Lake.instMonadTask_lake : Monad Task

Equations

• One or more equations did not get rendered due to their size.

@[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

@[implicit_reducible]

instance Lake.instMonadBaseIOTask : Monad BaseIOTask

Equations

• Lake.instMonadBaseIOTask = inferInstanceAs (Monad Task)

@[implicit_reducible]

instance Lake.instInhabitedBaseIOTask {α : Type u_1} [Inhabited α] : Inhabited (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

@[implicit_reducible]

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

Equations

• Lake.instInhabitedOptionIOTask = { default := failure }