From 1eaae47bab46479b10d043763ff20d9fa2f3ef38 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 May 2020 14:47:24 -0700
Subject: [PATCH] fix: add `Std` to builtin path

---
 src/Init/Lean/Util/Path.lean | 7 +++++--
 src/Std.lean                 | 6 ++++++
 2 files changed, 11 insertions(+), 2 deletions(-)
 create mode 100644 src/Std.lean

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