Documentation

Lean.Util.Path

partial def Lean.forEachModuleInDir {m : TypeType u_1} [Monad m] [MonadLiftT IO m] (dir : Lake.FilePath) (f : Lake.Namem PUnit) :

Executes f with the corresponding module name for each .lean file contained in dir.

For example, if dir contains A/B/C.lean, f is called with A.B.C.

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

        A `.olean' search path.

        Equations
        Instances For

          If the package of mod can be found in sp, return the path with extension ext (lean or olean) corresponding to mod. Otherwise, return none. Does not check whether the returned path exists.

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

            Like findWithExt, but ensures the returned path exists.

            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
                @[export lean_get_prefix]
                Equations
                Instances For
                  @[export lean_get_libdir]
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For

                        Initialize Lean's search path given Lean's system root and an initial search path. The system root can be obtained via getBuildDir (for internal use) or findSysroot (for external users).

                        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
                            @[export lean_module_name_of_file]

                            Infer module name of source file name.

                            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

                                Find the system root of the given lean command by calling lean --print-prefix and returning the path it prints. Defaults to trying the lean in PATH. If set, the LEAN_SYSROOT environment variable takes precedence. Note that the called lean binary might not be part of the system root, e.g. in the case of elan's proxy binary. Users internal to Lean should use Lean.getBuildDir instead.

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