structure Lake.Context : Type

A Lake configuration.

• opaqueWs : Lake.OpaqueWorkspace

@[inline, reducible]

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 : Lake.Context) (self : Lake.LakeT m α) : m α

Equations

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

@[inline, reducible]

abbrev Lake.LakeM (α : Type) : Type

A monad equipped with a Lake.Context.

Equations

• Lake.LakeM = Lake.LakeT Id

@[inline]

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

Equations

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