Documentation

Lake.Build.Library

Library Facet Builds #

Build function definitions for a library's builtin facets.

Build Lean & Static Lib #

source
def Lake.LeanLib.elabArtsFacetConfig :
LibraryFacetConfig elabArtsFacet

The LibraryFacetConfig for the builtin elabArtsFacet.

Equations
Instances For
    source
    def Lake.LeanLib.irArtsFacetConfig :
    LibraryFacetConfig irArtsFacet

    The LibraryFacetConfig for the builtin irArtsFacet.

    Equations
    Instances For
      source
      def Lake.LeanLib.leanArtsFacetConfig :
      LibraryFacetConfig leanArtsFacet

      The LibraryFacetConfig for the builtin leanArtsFacet.

      Equations
      Instances For
        source
        def Lake.LeanLib.staticFacetConfig :
        LibraryFacetConfig staticFacet

        The LibraryFacetConfig for the builtin staticFacet.

        Equations
        Instances For
          source
          def Lake.LeanLib.staticExportFacetConfig :
          LibraryFacetConfig staticExportFacet

          The LibraryFacetConfig for the builtin staticExportFacet.

          Equations
          Instances For

            Build Shared Lib #

            source
            def Lake.LeanLib.sharedFacetConfig :
            LibraryFacetConfig sharedFacet

            The LibraryFacetConfig for the builtin sharedFacet.

            Equations
            Instances For

              Other #

              source
              def Lake.LeanLib.extraDepFacetConfig :
              LibraryFacetConfig extraDepFacet

              The LibraryFacetConfig for the builtin extraDepFacet.

              Equations
              Instances For
                source
                def Lake.LeanLib.defaultFacetConfig :
                LibraryFacetConfig defaultFacet

                The LibraryFacetConfig for the builtin defaultFacet.

                Equations
                Instances For
                  source
                  def Lake.LeanLib.initFacetConfigs :
                  DNameMap LeanLibFacetConfig

                  A name-configuration map for the initial set of Lean library facets (e.g., lean, static, shared).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Lake.initLibraryFacetConfigs :
                    DNameMap LibraryFacetConfig

                    A name-configuration map for the initial set of Lean library facets (e.g., lean, static, shared).

                    Equations
                    Instances For