diff --git a/src/Init/Lean/Util/Path.lean b/src/Init/Lean/Util/Path.lean index 6b01372943..47da742418 100644 --- a/src/Init/Lean/Util/Path.lean +++ b/src/Init/Lean/Util/Path.lean @@ -49,8 +49,11 @@ appDir ← IO.appDir; let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Init"; installedLibDirExists ← IO.isDir installedLibDir; if installedLibDirExists then do - path ← realPathNormalized installedLibDir; - pure $ HashMap.empty.insert "Init" path + initPath ← realPathNormalized installedLibDir; + let map := HashMap.empty.insert "Init" initPath; + let stdDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Std"; + stdPath ← realPathNormalized stdDir; + pure $ map.insert "Std" stdPath else pure ∅ diff --git a/src/Std.lean b/src/Std.lean new file mode 100644 index 0000000000..350c0228e1 --- /dev/null +++ b/src/Std.lean @@ -0,0 +1,6 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Std.Data