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.instConfigMeta : ConfigInfo `Lake.WorkspaceConfig

Equations

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

instance Lake.WorkspaceConfig.instConfigFields : ConfigFields WorkspaceConfig

Equations

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

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

Equations

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

instance Lake.instInhabitedWorkspaceConfig : Inhabited WorkspaceConfig

Equations

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

instance Lake.instReprWorkspaceConfig : Repr WorkspaceConfig

Equations

• Lake.instReprWorkspaceConfig = { reprPrec := Lake.reprWorkspaceConfig✝ }

instance Lake.instEmptyCollectionWorkspaceConfig : EmptyCollection WorkspaceConfig

Equations

• Lake.instEmptyCollectionWorkspaceConfig = { emptyCollection := { } }