structure Lake.Context : Type

• opaqueWs : Lake.OpaqueWorkspace

A Lake configuration.

@[inline, reducible]

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

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

@[inline]

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

@[inline, reducible]

abbrev Lake.LakeM (α : Type) : Type

A monad equipped with a Lake.Context.

@[inline]

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