Instances For
Equations
- Lean.modToFilePath.go base (Lean.Name.str p h) = Lean.modToFilePath.go base p / { toString := h }
- Lean.modToFilePath.go base Lean.Name.anonymous = base
- Lean.modToFilePath.go base (Lean.Name.num pre i) = panicWithPosWithDecl "Lean.Util.Path" "Lean.modToFilePath.go" 25 20 "ill-formed import"
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.
Instances For
Like findWithExt, but ensures the returned path exists.
Instances For
Instances For
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).
Instances For
Infer module name of source file name.
Instances For
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.