structure Lake.WorkspaceConfig : Type

A Workspace's declarative configuration.

• packagesDir : Lake.FilePath

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

instance Lake.instInhabitedWorkspaceConfig : Inhabited Lake.WorkspaceConfig

Equations

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

instance Lake.instReprWorkspaceConfig : Repr Lake.WorkspaceConfig

Equations

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