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).

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