structure Lake.Context : Type

A Lake configuration.

• opaqueWs : OpaqueWorkspace

@[reducible, inline]

abbrev Lake.LakeT (m : Type → Type u_1) (α : Type) : Type u_1

A transformer to equip a monad with a Lake.Context.

Equations

• Lake.LakeT = ReaderT Lake.Context

@[inline]

def Lake.LakeT.run {m : Type → Type u_1} {α : Type} (ctx : Context) (self : LakeT m α) : m α

Equations

• Lake.LakeT.run ctx self = ReaderT.run self ctx

@[reducible, inline]

abbrev Lake.LakeM (α : Type) : Type

A monad equipped with a Lake.Context.

Equations

• Lake.LakeM = Lake.LakeT Id

Instances For

• Lake.instMonadLiftLakeMBuildTOfPure

@[inline]

def Lake.LakeM.run {α : Type} (ctx : Context) (self : LakeM α) : α

Equations

• Lake.LakeM.run ctx self = (ReaderT.run self ctx).run