Documentation

Lake.Build.Imports

Definitions to support lake setup-file builds.

Builds an Array of module imports for a Lean file. Used by lake setup-file to build modules for the Lean server and by lake lean to build the imports of a file. Returns the set of module dynlibs built (so they can be loaded by Lean).

Instances For