structure Lake.WorkspaceConfig : Type

A Workspace's declarative configuration.

• packagesDir : System.FilePath

  The directory to which Lake should download remote dependencies. Defaults to defaultPackagesDir (i.e., .lake/packages).

instance Lake.WorkspaceConfig.instEmptyCollection : EmptyCollection WorkspaceConfig

Equations

• Lake.WorkspaceConfig.instEmptyCollection = { emptyCollection := { } }

instance Lake.WorkspaceConfig.packagesDir.instConfigField : ConfigField WorkspaceConfig `packagesDir System.FilePath

Equations

• Lake.WorkspaceConfig.packagesDir.instConfigField = { toConfigProj := Lake.WorkspaceConfig.packagesDir._proj }

instance Lake.WorkspaceConfig.instConfigInfo : ConfigInfo `Lake.WorkspaceConfig

Equations

• Lake.WorkspaceConfig.instConfigInfo = { fields := Lake.WorkspaceConfig._fields }

instance Lake.WorkspaceConfig.instConfigFields : ConfigFields WorkspaceConfig

Equations

• Lake.WorkspaceConfig.instConfigFields = { fields := Lake.WorkspaceConfig._fields }

def Lake.instInhabitedWorkspaceConfig.default : WorkspaceConfig

Equations

• Lake.instInhabitedWorkspaceConfig.default = { packagesDir := default }

instance Lake.instInhabitedWorkspaceConfig : Inhabited WorkspaceConfig

Equations

• Lake.instInhabitedWorkspaceConfig = { default := Lake.instInhabitedWorkspaceConfig.default }

def Lake.instReprWorkspaceConfig.repr : WorkspaceConfig → Nat → Std.Format

Equations

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

instance Lake.instReprWorkspaceConfig : Repr WorkspaceConfig

Equations

• Lake.instReprWorkspaceConfig = { reprPrec := Lake.instReprWorkspaceConfig.repr }