Documentation

Lake.Config.Module

structure Lake.Module :

A buildable Lean module of a LeanLib.

  • lib : LeanLib
  • name : Lean.Name
  • keyName : Lean.Name

    The name of the module as a key. Used to create private modules (e.g., executable roots).

Instances For
    @[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
                          Instances For

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

                            Equations
                              Instances For

                                Returns the buildable module in the library whose source file is path.

                                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
                                          Instances For

                                            The library's buildable root modules.

                                            Equations
                                              Instances For
                                                @[reducible, inline]
                                                abbrev Lake.Module.pkg (self : Module) :
                                                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
                                                                                                @[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
                                                                                                                                  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
                                                                                                                                                                                    @[inline]
                                                                                                                                                                                    Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[inline]
                                                                                                                                                                                        Equations
                                                                                                                                                                                          Instances For

                                                                                                                                                                                            Trace Helpers #

                                                                                                                                                                                            Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                Equations
                                                                                                                                                                                                  Instances For