Lean.Util.Paths

structure Lean.LeanPaths :

Type

Equations

Equations

Equations

Lean.initSrcSearchPath leanSysroot sp = do let a ← liftM (IO.getEnv "LEAN_SRC_PATH") let srcSearchPath : Lean.SearchPath := match a with | some p => System.SearchPath.parse p | x => [] let a ← IO.appDir let srcPath : System.FilePath := a / { toString := ".." } / { toString := "src" } / { toString := "lean" } pure (srcSearchPath ++ [srcPath / { toString := "lake" }, srcPath])