Documentation

Lake.Build.Executable

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