Documentation

Lake.Build.Executable

← Mathematical handbook

Lean Executable Build #

The build function definition for a Lean executable.

source
def Lake.LeanExe.exeFacetConfig :
LeanExeFacetConfig exeFacet

The facet configuration for the builtin LeanExe.exeFacet.

Equations
Instances For
    source
    def Lake.LeanExe.defaultFacetConfig :
    LeanExeFacetConfig defaultFacet

    The facet configuration for the builtin ExternLib.dynlibFacet.

    Equations
    Instances For
      source
      def Lake.LeanExe.initFacetConfigs :
      DNameMap LeanExeFacetConfig

      A name-configuration map for the initial set of Lean executable facets (e.g., exe).

      Equations
      Instances For