The require
syntax #
This module contains the expansion of the require
DSL syntax used to specify package dependencies.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Adds a new package dependency to the workspace. The general syntax is:
require ["<scope>" /] <pkg-name> [@ <version>]
[from <source>] [with <options>]
The from
clause tells Lake where to locate the dependency.
See the fromClause
syntax documentation (e.g., hover over it) to see
the different forms this clause can take.
Without a from
clause, Lake will lookup the package in the default
registry (i.e., Reservoir) and use the information there to download the
package at the requested version
. The scope
is used to disambiguate between
packages in the registry with the same pkg-name
. In Reservoir, this scope
is the package owner (e.g., leanprover
of @leanprover/doc-gen4
).
The with
clause specifies a NameMap String
of Lake options
used to configure the dependency. This is equivalent to passing -K
options to the dependency on the command line.
Equations
- Lake.DSL.RequireDecl = Lean.TSyntax `Lake.DSL.requireDecl
Instances For
Equations
- Lake.DSL.instCoeRequireDeclCommand = { coe := fun (x : Lake.DSL.RequireDecl) => { raw := x.raw } }