def Lake.DSL.packageDeclName : Lake.Name

The name given to the definition created by the package syntax.

Equations

• Lake.DSL.packageDeclName = `_package

def Lake.DSL.packageDecl : Lean.ParserDescr

Defines the configuration of a Lake package. Has many forms:

package «pkg-name»
package «pkg-name» { /- config opts -/ }
package «pkg-name» where /- config opts -/
package «pkg-name» : PackageConfig := /- config -/

There can only be one package declaration per Lake configuration file. The defined package configuration will be available for reference as _package.

Equations

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