Documentation

Lake.Config.Module

structure Lake.Module :

A buildable Lean module of a LeanLib.

Instances For
    Equations
    Equations
    @[reducible, inline]
    Equations
    Instances For
      @[inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[inline]
          Equations
          Instances For
            @[reducible, inline]
            abbrev Lake.ModuleMap (α : Type u_1) :
            Type u_1
            Equations
            Instances For
              @[inline]
              Equations
              • Lake.ModuleMap.empty = Lean.RBMap.empty
              Instances For

                Locate the named, buildable module in the library (which implies it is local and importable).

                Equations
                Instances For

                  Locate the named, buildable, importable, local module in the package.

                  Equations
                  Instances For

                    Get an Array of the library's modules (as specified by its globs).

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

                      The library's buildable root modules.

                      Equations
                      Instances For
                        @[reducible, inline]
                        Equations
                        • self.pkg = self.lib.pkg
                        Instances For
                          @[inline]
                          Equations
                          • self.rootDir = self.lib.rootDir
                          Instances For
                            @[inline]
                            Equations
                            Instances For
                              @[inline]
                              Equations
                              Instances For
                                @[inline]
                                Equations
                                Instances For
                                  @[inline]
                                  Equations
                                  Instances For
                                    @[inline]
                                    Equations
                                    Instances For
                                      @[inline]
                                      Equations
                                      Instances For
                                        @[inline]
                                        Equations
                                        Instances For
                                          @[inline]
                                          Equations
                                          Instances For
                                            @[inline]
                                            Equations
                                            Instances For
                                              @[inline]
                                              Equations
                                              Instances For
                                                @[inline]
                                                Equations
                                                Instances For
                                                  @[inline]
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      @[inline]
                                                      Equations
                                                      Instances For

                                                        Suffix for single module dynlibs (e.g., for precompilation).

                                                        Equations
                                                        Instances For
                                                          @[inline]
                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              Equations
                                                              • self.serverOptions = self.lib.serverOptions
                                                              Instances For
                                                                @[inline]
                                                                Equations
                                                                • self.buildType = self.lib.buildType
                                                                Instances For
                                                                  @[inline]
                                                                  Equations
                                                                  • self.backend = self.lib.backend
                                                                  Instances For
                                                                    @[inline]
                                                                    Equations
                                                                    • self.leanArgs = self.lib.leanArgs
                                                                    Instances For
                                                                      @[inline]
                                                                      Equations
                                                                      • self.weakLeanArgs = self.lib.weakLeanArgs
                                                                      Instances For
                                                                        @[inline]
                                                                        Equations
                                                                        • self.leancArgs = self.lib.leancArgs
                                                                        Instances For
                                                                          @[inline]
                                                                          Equations
                                                                          • self.weakLeancArgs = self.lib.weakLeancArgs
                                                                          Instances For
                                                                            @[inline]
                                                                            Equations
                                                                            • self.linkArgs = self.lib.linkArgs
                                                                            Instances For
                                                                              @[inline]
                                                                              Equations
                                                                              • self.weakLinkArgs = self.lib.weakLinkArgs
                                                                              Instances For
                                                                                @[inline]
                                                                                Equations
                                                                                • self.platformIndependent = self.lib.platformIndependent
                                                                                Instances For
                                                                                  @[inline]
                                                                                  Equations
                                                                                  • self.shouldPrecompile = self.lib.precompileModules
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    Equations
                                                                                    • self.nativeFacets shouldExport = self.lib.nativeFacets shouldExport
                                                                                    Instances For

                                                                                      Trace Helpers #

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