Documentation

Lake.Config.Module

structure Lake.Module :

A buildable Lean module of a LeanLib.

Instances For
    @[inline, reducible]
    Instances For
      @[inline]
      Instances For
        @[inline, reducible]
        Instances For
          @[inline, reducible]
          abbrev Lake.ModuleMap (α : Type u_1) :
          Type u_1
          Instances For
            @[inline]
            Instances For

              Locate the named module in the library (if it is buildable and local to it).

              Instances For

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

                Instances For

                  The library's buildable root modules.

                  Instances For
                    @[inline, reducible]
                    Instances For
                      @[inline]
                      Instances For
                        @[inline]
                        Instances For
                          @[inline]
                          Instances For
                            @[inline]
                            Instances For
                              @[inline]
                              Instances For
                                @[inline]
                                Instances For
                                  @[inline]
                                  Instances For
                                    @[inline]
                                    Instances For
                                      @[inline]
                                      Instances For
                                        @[inline]
                                        Instances For
                                          @[inline]
                                          Instances For

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

                                            Instances For
                                              @[inline]
                                              Instances For
                                                @[inline]
                                                Instances For
                                                  @[inline]
                                                  Instances For
                                                    @[inline]
                                                    Instances For
                                                      @[inline]
                                                      Instances For
                                                        @[inline]
                                                        Instances For
                                                          @[inline]
                                                          Instances For
                                                            @[inline]
                                                            Instances For
                                                              @[inline]
                                                              Instances For
                                                                @[inline]
                                                                Instances For

                                                                  Trace Helpers #